ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>F : TopCat.Presheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<VAR>x : ↑X<VAR>mU : x ∈ U<VAR>mV : x ∈ V<VAR>s : (CategoryTheory.forget C).obj (F.obj (Opposite.op U))<VAR>t : (CategoryTheory.forget C).obj (F.obj (Opposite.op V))<VAR>h : (F.germ ⟨x, mU⟩) s = (F.germ ⟨x, mV⟩) t<GOAL>∃ W, ∃ (_ : x ∈ W), ∃ iU iV, (F.map iU.op) s = (F.map iV.op) t
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>F G : TopCat.Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(f.app (Opposite.op U))<VAR>x : ↑X<GOAL>Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C x).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F : TopCat.Sheaf C X<VAR>U : TopologicalSpace.Opens ↑X<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op U))<VAR>h : ∀ (x : ↥U), (F.presheaf.germ x) s = (F.presheaf.germ x) t<GOAL>s = t
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F : TopCat.Sheaf C X<VAR>G : TopCat.Presheaf C X<VAR>f : F.val ⟶ G<VAR>U : TopologicalSpace.Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C ↑x).map f)<GOAL>Function.Injective ⇑(f.app (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F : TopCat.Sheaf C X<VAR>G : TopCat.Presheaf C X<VAR>f : F.val ⟶ G<GOAL>(∀ (x : ↑X), Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C x).map f)) ↔ ∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(f.app (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<VAR>CategoryTheory.Mono f<VAR>x : ↑X<GOAL>CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.val)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<VAR>∀ (x : ↑X), CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.val)<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<GOAL>CategoryTheory.Mono f ↔ ∀ (x : ↑X), CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.val)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<VAR>U : TopologicalSpace.Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (CategoryTheory.forget C).obj (G.val.obj (Opposite.op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (Opposite.op V)) s = (G.val.map iVU.op) t<GOAL>Function.Surjective ⇑(f.val.app (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<VAR>U : TopologicalSpace.Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((TopCat.Presheaf.stalkFunctor C ↑x).map f.val)<GOAL>Function.Surjective ⇑(f.val.app (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<VAR>U : TopologicalSpace.Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((TopCat.Presheaf.stalkFunctor C ↑x).map f.val)<GOAL>Function.Bijective ⇑(f.val.app (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<VAR>U : TopologicalSpace.Opens ↑X<VAR>∀ (x : ↥U), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C ↑x).map f.val)<GOAL>CategoryTheory.IsIso (f.val.app (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<VAR>∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.val)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>F G : TopCat.Sheaf C X<VAR>f : F ⟶ G<GOAL>CategoryTheory.IsIso f ↔ ∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.val)
<VAR>X : TopCat<VAR>F : TopCat.Presheaf CommRingCat X<VAR>U : TopologicalSpace.Opens ↑X<VAR>x : ↥U<GOAL>algebraMap ↑(F.obj (Opposite.op U)) ↑(F.stalk ↑x) = F.germ x
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<GOAL>𝓝 = Function.update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Set.Iio γ))
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<GOAL>𝓝 0 = ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Set.Iio γ)
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<GOAL>(𝓝 0).HasBasis (fun γ => γ ≠ 0) Set.Iio
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>γ : Γ₀<VAR>hγ : γ ≠ 0<GOAL>Set.Iio γ ∈ 𝓝 0
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>γ : Γ₀ˣ<GOAL>Set.Iio ↑γ ∈ 𝓝 0
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<GOAL>Filter.Tendsto f l (𝓝 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>γ : Γ₀<VAR>h₀ : γ ≠ 0<GOAL>𝓝 γ = pure γ
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>γ : Γ₀ˣ<GOAL>𝓝 ↑γ = pure ↑γ
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>γ : Γ₀ˣ<GOAL>{↑γ} ∈ 𝓝 ↑γ
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>γ : Γ₀<VAR>h : γ ≠ 0<GOAL>{γ} ∈ 𝓝 γ
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>x : Γ₀<VAR>h : x ≠ 0<GOAL>(𝓝 x).HasBasis (fun x => True) fun x_1 => {x}
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>γ : Γ₀ˣ<GOAL>(𝓝 ↑γ).HasBasis (fun x => True) fun x => {↑γ}
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>γ : Γ₀<VAR>h : γ ≠ 0<GOAL>Filter.Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>γ₀ : Γ₀ˣ<GOAL>Filter.Tendsto f l (𝓝 ↑γ₀) ↔ ∀ᶠ (x : α) in l, f x = ↑γ₀
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>γ₁ γ₂ : Γ₀<VAR>h : γ₁ < γ₂<GOAL>Set.Iio γ₂ ∈ 𝓝 γ₁
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>s : Set Γ₀<GOAL>IsOpen s ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Set.Iio γ ⊆ s
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>s : Set Γ₀<GOAL>IsClosed s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Set.Ici γ
<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>a : Γ₀<GOAL>IsOpen (Set.Iio a)
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosed<GOAL>f.IsClosable
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hf : f.IsClosable<VAR>hfg : g ≤ f<GOAL>g.IsClosable
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>∃! f', f.graph.topologicalClosure = f'.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>f.closure = Exists.choose hf
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : ¬f.IsClosable<GOAL>f.closure = f
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>f.graph.topologicalClosure = f.closure.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<GOAL>f ≤ f.closure
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hg : g.IsClosable<VAR>h : f ≤ g<GOAL>f.closure ≤ g.closure
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>f.closure.IsClosed
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>f.closure.IsClosable
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<GOAL>f.IsClosable ↔ ∃ g, g.IsClosed ∧ f ≤ g
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>S : Submodule R E<VAR>self : f.HasCore S<GOAL>S ≤ f.domain
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>S : Submodule R E<VAR>self : f.HasCore S<GOAL>(f.domRestrict S).closure = f
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>S : Submodule R E<VAR>h : f.HasCore S<GOAL>(f.domRestrict S).closure = f
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<GOAL>f.closure.HasCore f.domain
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>f.closure.inverse.graph = f.inverse.graph.topologicalClosure
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<GOAL>f.inverse.IsClosable ↔ LinearMap.ker f.closure.toFun = ⊥
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing R<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module R E<VAR>Module R F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>ContinuousAdd E<VAR>ContinuousAdd F<VAR>TopologicalSpace R<VAR>ContinuousSMul R E<VAR>ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>f.inverse.closure = f.closure.inverse
<VAR>M : Type u_1<VAR>Nonempty M<VAR>Semigroup M<VAR>TopologicalSpace M<VAR>CompactSpace M<VAR>T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<GOAL>∃ m, m * m = m
<VAR>M : Type u_1<VAR>Nonempty M<VAR>AddSemigroup M<VAR>TopologicalSpace M<VAR>CompactSpace M<VAR>T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x + r<GOAL>∃ m, m + m = m
<VAR>M : Type u_1<VAR>Semigroup M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>s : Set M<VAR>snemp : s.Nonempty<VAR>s_compact : IsCompact s<VAR>s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s<GOAL>∃ m ∈ s, m * m = m
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x + r<VAR>s : Set M<VAR>snemp : s.Nonempty<VAR>s_compact : IsCompact s<VAR>s_add : ∀ x ∈ s, ∀ y ∈ s, x + y ∈ s<GOAL>∃ m ∈ s, m + m = m
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>SubmodulesRingBasis fun n => I ^ n • ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>NonarchimedeanRing R
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>(𝓝 0).HasBasis (fun _n => True) fun n => ↑(I ^ n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>x : R<GOAL>(𝓝 x).HasBasis (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>I.ringFilterBasis.SubmodulesBasis fun n => I ^ n • ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>top : TopologicalSpace R<VAR>TopologicalRing R<VAR>J : Ideal R<GOAL>IsAdic J ↔ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
<VAR>R : Type u_1<VAR>CommRing R<VAR>TopologicalSpace R<VAR>TopologicalRing R<VAR>J : Ideal R<VAR>h : IsAdic J<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>IsAdic (J ^ n)
<VAR>A : Type u_2<VAR>CommRing A<VAR>TopologicalSpace A<VAR>TopologicalRing A<GOAL>IsAdic ⊥ ↔ DiscreteTopology A
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>DecidableEq ι<VAR>TopologicalSpace F<GOAL>Set.range ContinuousMultilinearMap.toUniformOnFun = {f | Continuous ((UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f) ∧ (∀ (m : (i : ι) → E i) (i : ι) (x y : E i), (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (x + y)) = (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x) + (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i y)) ∧ ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i), (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (c • x)) = c • (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x)}
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>f : ContinuousMultilinearMap 𝕜 E F<GOAL>(UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f.toUniformOnFun = ⇑f
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>UniformSpace F<VAR>UniformAddGroup F<GOAL>UniformEmbedding ContinuousMultilinearMap.toUniformOnFun
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>UniformSpace F<VAR>UniformAddGroup F<GOAL>Embedding ContinuousMultilinearMap.toUniformOnFun
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>∀ (i : ι), ContinuousSMul 𝕜 (E i)<GOAL>UniformContinuous DFunLike.coe
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>∀ (i : ι), ContinuousSMul 𝕜 (E i)<VAR>x : (i : ι) → E i<GOAL>UniformContinuous fun f => f x
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>∀ (i : ι), ContinuousSMul 𝕜 (E i)<VAR>ContinuousConstSMul 𝕜 F<VAR>CompleteSpace F<VAR>T2Space F<VAR>h : RestrictGenTopology {s | Bornology.IsVonNBounded 𝕜 s}<GOAL>CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<GOAL>∀ {ι_1 : Type u_5} {p : ι_1 → Prop} {b : ι_1 → Set F}, (𝓝 0).HasBasis p b → (𝓝 0).HasBasis (fun Si => Bornology.IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | Set.MapsTo (⇑f) Si.1 (b Si.2)}
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<GOAL>(𝓝 0).HasBasis (fun SV => Bornology.IsVonNBounded 𝕜 SV.1 ∧ SV.2 ∈ 𝓝 0) fun SV => {f | Set.MapsTo (⇑f) SV.1 SV.2}
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>∀ (i : ι), ContinuousSMul 𝕜 (E i)<VAR>x : (i : ι) → E i<GOAL>Continuous fun p => p x
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>∀ (i : ι), ContinuousSMul 𝕜 (E i)<GOAL>Continuous DFunLike.coe
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>∀ (i : ι), ContinuousSMul 𝕜 (E i)<VAR>ContinuousConstSMul 𝕜 F<VAR>m : (i : ι) → E i<VAR>c : ContinuousMultilinearMap 𝕜 E F<GOAL>(ContinuousMultilinearMap.apply 𝕜 E F m) c = c m