ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto (fun x => ↑⌈x⌉) (𝓝[>] ↑n) (𝓝 (↑n + 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>n : ℤ<GOAL>ContinuousOn Int.fract (Set.Ico (↑n) (↑n + 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>TopologicalAddGroup α<VAR>x : α<VAR>h : x ≠ ↑⌊x⌋<GOAL>ContinuousAt Int.fract x
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>TopologicalAddGroup α<VAR>n : ℤ<GOAL>Filter.Tendsto Int.fract (𝓝[<] ↑n) (𝓝 1)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>TopologicalAddGroup α<VAR>n : ℤ<GOAL>Filter.Tendsto Int.fract (𝓝[<] ↑n) (𝓝[<] 1)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>TopologicalAddGroup α<VAR>n : ℤ<GOAL>Filter.Tendsto Int.fract (𝓝[≥] ↑n) (𝓝 0)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>TopologicalAddGroup α<VAR>n : ℤ<GOAL>Filter.Tendsto Int.fract (𝓝[≥] ↑n) (𝓝[≥] 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : β → α → γ<VAR>h : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1)<VAR>hf : ∀ (s : β), f s 0 = f s 1<GOAL>Continuous fun st => f st.1 (Int.fract st.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>s : β → α<VAR>f : β → α → γ<VAR>h : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1)<VAR>hs : Continuous s<VAR>hf : ∀ (s : β), f s 0 = f s 1<GOAL>Continuous fun x => f x (Int.fract (s x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : ContinuousOn f (Set.Icc 0 1)<VAR>hf : f 0 = f 1<GOAL>Continuous (f ∘ Int.fract)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Zero β<VAR>TopologicalSpace β<VAR>self : α →C₀ β<GOAL>Filter.Tendsto self.toFun (Filter.cocompact α) (𝓝 0)
<VAR>F : Type u_2<VAR>α : outParam (Type u_3)<VAR>β : outParam (Type u_4)<VAR>TopologicalSpace α<VAR>Zero β<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>self : ZeroAtInftyContinuousMapClass F α β<VAR>f : F<GOAL>Filter.Tendsto (⇑f) (Filter.cocompact α) (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α →C₀ β<GOAL>⇑f.toContinuousMap = ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f g : α →C₀ β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α →C₀ β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α →C₀ β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>IsEmpty α<VAR>f g : α →C₀ β<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>CompactSpace α<VAR>f : α →C₀ β<GOAL>ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty.symm f = ↑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>CompactSpace α<VAR>f : C(α, β)<VAR>a : α<GOAL>(ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty f) a = f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>G : Type u_2<VAR>FunLike G α β<VAR>ContinuousMapClass G α β<VAR>CompactSpace α<GOAL>ZeroAtInftyContinuousMapClass G α β
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<GOAL>⇑0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>Zero β<GOAL>0 x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>MulZeroClass β<VAR>ContinuousMul β<VAR>f g : α →C₀ β<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>MulZeroClass β<VAR>ContinuousMul β<VAR>f g : α →C₀ β<GOAL>(f * g) x = f x * g x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddZeroClass β<VAR>ContinuousAdd β<VAR>f g : α →C₀ β<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>AddZeroClass β<VAR>ContinuousAdd β<VAR>f g : α →C₀ β<GOAL>(f + g) x = f x + g x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>R : Type u_2<VAR>Zero R<VAR>SMulWithZero R β<VAR>ContinuousConstSMul R β<VAR>r : R<VAR>f : α →C₀ β<GOAL>⇑(r • f) = r • ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>R : Type u_2<VAR>Zero R<VAR>SMulWithZero R β<VAR>ContinuousConstSMul R β<VAR>r : R<VAR>f : α →C₀ β<VAR>x : α<GOAL>(r • f) x = r • f x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f : α →C₀ β<GOAL>⇑(-f) = -⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f : α →C₀ β<GOAL>(-f) x = -f x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f g : α →C₀ β<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f g : α →C₀ β<GOAL>(f - g) x = f x - g x
<VAR>F : Type u_1<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>Zero γ<VAR>FunLike F β γ<VAR>ZeroAtInftyContinuousMapClass F β γ<VAR>f : F<GOAL>UniformContinuous ⇑f
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>FunLike F α β<VAR>ZeroAtInftyContinuousMapClass F α β<VAR>f : F<GOAL>∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>f : α →C₀ β<GOAL>Bornology.IsBounded (Set.range ⇑f)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>f : α →C₀ β<VAR>s : Set α<GOAL>Bornology.IsBounded (⇑f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>f : α →C₀ β<VAR>a : α<GOAL>f.toBCF a = f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<GOAL>Function.Injective ZeroAtInftyContinuousMap.toBCF
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>f g : α →C₀ β<GOAL>dist f.toBCF g.toBCF = dist f g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>ι : Type u_2<VAR>F : ι → α →C₀ β<VAR>f : α →C₀ β<VAR>l : Filter ι<GOAL>Filter.Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => ⇑(F i)) (⇑f) l
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<GOAL>Isometry ZeroAtInftyContinuousMap.toBCF
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<GOAL>IsClosed (Set.range ZeroAtInftyContinuousMap.toBCF)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : α →C₀ β<GOAL>‖f.toBCF‖ = ‖f‖
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddMonoid β<VAR>StarAddMonoid β<VAR>ContinuousStar β<VAR>f : α →C₀ β<GOAL>⇑(star f) = star ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddMonoid β<VAR>StarAddMonoid β<VAR>ContinuousStar β<VAR>f : α →C₀ β<VAR>x : α<GOAL>(star f) x = star (f x)
<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>Zero δ<VAR>f : γ →C₀ δ<VAR>g : CocompactMap β γ<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>γ : Type w<VAR>δ : Type u_2<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>Zero δ<VAR>f : γ →C₀ δ<GOAL>f.comp (CocompactMap.id γ) = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>δ : Type u_2<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>Zero δ<VAR>f : γ →C₀ δ<VAR>g : CocompactMap β γ<VAR>h : CocompactMap α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>Zero δ<VAR>g : CocompactMap β γ<GOAL>ZeroAtInftyContinuousMap.comp 0 g = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ConditionallyCompleteLinearOrder X<VAR>DenselyOrdered X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>LinearOrder Y<VAR>TopologicalSpace Y<VAR>OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hfI : f a = f b<GOAL>∃ c ∈ Set.Ioo a b, IsExtrOn f (Set.Icc a b) c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ConditionallyCompleteLinearOrder X<VAR>DenselyOrdered X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>LinearOrder Y<VAR>TopologicalSpace Y<VAR>OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hfI : f a = f b<GOAL>∃ c ∈ Set.Ioo a b, IsLocalExtr f c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ConditionallyCompleteLinearOrder X<VAR>DenselyOrdered X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>LinearOrder Y<VAR>TopologicalSpace Y<VAR>OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Ioo a b)<VAR>ha : Filter.Tendsto f (𝓝[>] a) (𝓝 l)<VAR>hb : Filter.Tendsto f (𝓝[<] b) (𝓝 l)<GOAL>∃ c ∈ Set.Ioo a b, IsExtrOn f (Set.Ioo a b) c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ConditionallyCompleteLinearOrder X<VAR>DenselyOrdered X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>LinearOrder Y<VAR>TopologicalSpace Y<VAR>OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Ioo a b)<VAR>ha : Filter.Tendsto f (𝓝[>] a) (𝓝 l)<VAR>hb : Filter.Tendsto f (𝓝[<] b) (𝓝 l)<GOAL>∃ c ∈ Set.Ioo a b, IsLocalExtr f c
<VAR>K : Type u_1<VAR>hK : NormedField K<VAR>h : IsNonarchimedean norm<VAR>x : K<GOAL>(NormedField.valuation h) x = ‖x‖₊
<VAR>L : Type u_2<VAR>Field L<VAR>Γ₀ : Type u_3<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>val : Valued L Γ₀<VAR>hv : Valued.v.RankOne<VAR>x : L<GOAL>0 ≤ Valued.norm x
<VAR>L : Type u_2<VAR>Field L<VAR>Γ₀ : Type u_3<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>val : Valued L Γ₀<VAR>hv : Valued.v.RankOne<VAR>x y : L<GOAL>Valued.norm (x + y) ≤ max (Valued.norm x) (Valued.norm y)
<VAR>L : Type u_2<VAR>Field L<VAR>Γ₀ : Type u_3<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>val : Valued L Γ₀<VAR>hv : Valued.v.RankOne<VAR>x : L<VAR>hx : Valued.norm x = 0<GOAL>x = 0
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>Archimedean 𝕜<GOAL>DenseRange Rat.cast
<VAR>G : Type u_1<VAR>LinearOrderedAddCommGroup G<VAR>TopologicalSpace G<VAR>OrderTopology G<VAR>Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Set.Ioo 0 ε<GOAL>Dense ↑S
<VAR>G : Type u_1<VAR>LinearOrderedAddCommGroup G<VAR>TopologicalSpace G<VAR>OrderTopology G<VAR>Archimedean G<VAR>S : AddSubgroup G<VAR>hbot : S ≠ ⊥<VAR>H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a<GOAL>Dense ↑S
<VAR>G : Type u_1<VAR>LinearOrderedAddCommGroup G<VAR>TopologicalSpace G<VAR>OrderTopology G<VAR>Archimedean G<VAR>S : AddSubgroup G<GOAL>Dense ↑S ∨ ∃ a, S = AddSubgroup.closure {a}
<VAR>X : TopCat<VAR>F : TopCat.Presheaf (Type u) X<VAR>ι : Type x<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>sf : (i : ι) → (CategoryTheory.forget (Type u)).obj (F.obj (Opposite.op (U i)))<VAR>s : (CategoryTheory.forget (Type u)).obj (F.obj (Opposite.op (iSup U)))<GOAL>F.IsGluing U sf s ↔ ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ), (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op).π.app i s = TopCat.Presheaf.objPairwiseOfFamily sf i
<VAR>X : TopCat<VAR>F : TopCat.Presheaf (Type u) X<GOAL>F.IsSheaf ↔ F.IsSheafUniqueGluing
<VAR>X : TopCat<VAR>F : TopCat.Presheaf (Type u) X<VAR>Fsh : F.IsSheafUniqueGluing<GOAL>F.IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasLimits C<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheaf ↔ F.IsSheafUniqueGluing
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms<VAR>CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>ι : Type v<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (U i)))<VAR>h : TopCat.Presheaf.IsCompatible F.val U sf<GOAL>∃! s, TopCat.Presheaf.IsGluing F.val U sf s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms<VAR>CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>ι : Type v<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>V : TopologicalSpace.Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (U i)))<VAR>h : TopCat.Presheaf.IsCompatible F.val U sf<GOAL>∃! s, ∀ (i : ι), (F.val.map (iUV i).op) s = sf i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms<VAR>CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>ι : Type v<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (iSup U)))<VAR>h : ∀ (i : ι), (F.val.map (TopologicalSpace.Opens.leSupr U i).op) s = (F.val.map (TopologicalSpace.Opens.leSupr U i).op) t<GOAL>s = t
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms<VAR>CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>ι : Type v<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>V : TopologicalSpace.Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V))<VAR>h : ∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t<GOAL>s = t
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms<VAR>CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>U₁ U₂ V : TopologicalSpace.Opens ↑X<VAR>i₁ : U₁ ⟶ V<VAR>i₂ : U₂ ⟶ V<VAR>hcover : V ≤ U₁ ⊔ U₂<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V))<VAR>h₁ : (F.val.map i₁.op) s = (F.val.map i₁.op) t<VAR>h₂ : (F.val.map i₂.op) s = (F.val.map i₂.op) t<GOAL>s = t
<VAR>X : TopCat<VAR>F : TopCat.Sheaf CommRingCat X<VAR>U V W UW VW : TopologicalSpace.Opens ↑X<VAR>e : W ≤ U ⊔ V<VAR>x : ↥((RingHom.comp (F.val.map (CategoryTheory.homOfLE ⋯).op) (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus (RingHom.comp (F.val.map (CategoryTheory.homOfLE ⋯).op) (RingHom.snd ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))))<VAR>y : ↑(F.val.obj (Opposite.op W))<VAR>h₁ : UW = U ⊓ W<VAR>h₂ : VW = V ⊓ W<GOAL>(F.val.map (CategoryTheory.homOfLE e).op) ((F.objSupIsoProdEqLocus U V).inv x) = y ↔ (F.val.map (CategoryTheory.homOfLE ⋯).op) (↑x).1 = (F.val.map (CategoryTheory.homOfLE ⋯).op) y ∧ (F.val.map (CategoryTheory.homOfLE ⋯).op) (↑x).2 = (F.val.map (CategoryTheory.homOfLE ⋯).op) y
<VAR>R : Type u_1<VAR>𝕜 : Type u_2<VAR>NonUnitalNonAssocRing R<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace R<VAR>TopologicalAddGroup R<VAR>norm : R → 𝕜<VAR>norm_nonneg : ∀ (x : R), 0 ≤ norm x<VAR>norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y<VAR>nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}<GOAL>TopologicalRing R
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : Filter.Tendsto g l (𝓝 C)<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atTop
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Filter.Tendsto f l (𝓝 C)<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atTop
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : Filter.Tendsto g l (𝓝 C)<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atBot
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Filter.Tendsto f l (𝓝 C)<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atBot
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : Filter.Tendsto g l (𝓝 C)<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atBot
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : Filter.Tendsto g l (𝓝 C)<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atTop
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Filter.Tendsto f l (𝓝 C)<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atBot
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Filter.Tendsto f l (𝓝 C)<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atTop
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<GOAL>Filter.atTop⁻¹ = 𝓝[>] 0
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<GOAL>(𝓝[>] 0)⁻¹ = Filter.atTop
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<GOAL>Filter.Tendsto (fun x => x⁻¹) (𝓝[>] 0) Filter.atTop
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<GOAL>Filter.Tendsto (fun r => r⁻¹) Filter.atTop (𝓝[>] 0)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<GOAL>Filter.Tendsto (fun r => r⁻¹) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>a : 𝕜<VAR>h : Filter.Tendsto f l (𝓝 a)<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x / g x) l (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>h : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto f⁻¹ l (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>h : Filter.Tendsto f l (𝓝[>] 0)<GOAL>Filter.Tendsto f⁻¹ l Filter.atTop
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Filter.Tendsto (fun x => x ^ (-↑n)) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>n : ℤ<VAR>hn : n < 0<GOAL>Filter.Tendsto (fun x => x ^ n) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>n : ℤ<VAR>c : 𝕜<VAR>hn : n < 0<GOAL>Filter.Tendsto (fun x => c * x ^ n) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>n : ℕ<VAR>c d : 𝕜<GOAL>Filter.Tendsto (fun x => c * x ^ n) Filter.atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>n : ℕ<VAR>c d : 𝕜<VAR>hc : c ≠ 0<GOAL>Filter.Tendsto (fun x => c * x ^ n) Filter.atTop (𝓝 d) ↔ n = 0 ∧ c = d
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>n : ℤ<VAR>c d : 𝕜<VAR>hc : c ≠ 0<GOAL>Filter.Tendsto (fun x => c * x ^ n) Filter.atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>Filter.comap (fun x_1 => x * x_1) (𝓝[>] 0) = 𝓝[>] 0
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>x : 𝕜<VAR>hx : 0 < x<VAR>p : 𝕜 → Prop<VAR>h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε<GOAL>∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p (x * ε)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>CommGroup G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Filter.Tendsto f Filter.cofinite (𝓝 1)<GOAL>CauchySeq fun s => ∏ i ∈ s, f i
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>NonarchimedeanAddGroup G<VAR>f : α → G<VAR>hf : Filter.Tendsto f Filter.cofinite (𝓝 0)<GOAL>CauchySeq fun s => ∑ i ∈ s, f i
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>CommGroup G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>NonarchimedeanGroup G<VAR>CompleteSpace G<VAR>f : α → G<VAR>hf : Filter.Tendsto f Filter.cofinite (𝓝 1)<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>NonarchimedeanAddGroup G<VAR>CompleteSpace G<VAR>f : α → G<VAR>hf : Filter.Tendsto f Filter.cofinite (𝓝 0)<GOAL>Summable f
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>CommGroup G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>NonarchimedeanGroup G<VAR>CompleteSpace G<VAR>f : α → G<GOAL>Multipliable f ↔ Filter.Tendsto f Filter.cofinite (𝓝 1)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>NonarchimedeanAddGroup G<VAR>CompleteSpace G<VAR>f : α → G<GOAL>Summable f ↔ Filter.Tendsto f Filter.cofinite (𝓝 0)
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Continuous ⇑DomMulAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Continuous ⇑DomAddAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Continuous ⇑DomMulAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Continuous ⇑DomAddAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>DomAddAct.mkHomeomorph.toEquiv = DomAddAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>DomMulAct.mkHomeomorph.toEquiv = DomMulAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>⇑DomAddAct.mkHomeomorph = ⇑DomAddAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>⇑DomMulAct.mkHomeomorph = ⇑DomMulAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>⇑DomMulAct.mkHomeomorph.symm = ⇑DomMulAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>⇑DomAddAct.mkHomeomorph.symm = ⇑DomAddAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Inducing ⇑DomAddAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Inducing ⇑DomMulAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Embedding ⇑DomMulAct.mk