ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>ContinuousMul α<VAR>DecidableEq β<VAR>f : β → α<VAR>b : β<VAR>hf : Multipliable (Function.update f b 1)<GOAL>∏' (x : β), f x = f b * ∏' (x : β), if x = b then 1 else f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>ContinuousAdd α<VAR>DecidableEq β<VAR>f : β → α<VAR>b : β<VAR>hf : Summable (Function.update f b 0)<GOAL>∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>T2Space α<VAR>ContinuousMul α<VAR>s : Set β<VAR>hs : Multipliable (f ∘ Subtype.val)<VAR>hsc : Multipliable (f ∘ Subtype.val)<GOAL>(∏' (x : ↑s), f ↑x) * ∏' (x : ↑sᶜ), f ↑x = ∏' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>T2Space α<VAR>ContinuousAdd α<VAR>s : Set β<VAR>hs : Summable (f ∘ Subtype.val)<VAR>hsc : Summable (f ∘ Subtype.val)<GOAL>∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>T2Space α<VAR>ContinuousMul α<VAR>s t : Set β<VAR>hd : Disjoint s t<VAR>hs : Multipliable (f ∘ Subtype.val)<VAR>ht : Multipliable (f ∘ Subtype.val)<GOAL>∏' (x : ↑(s ∪ t)), f ↑x = (∏' (x : ↑s), f ↑x) * ∏' (x : ↑t), f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>T2Space α<VAR>ContinuousAdd α<VAR>s t : Set β<VAR>hd : Disjoint s t<VAR>hs : Summable (f ∘ Subtype.val)<VAR>ht : Summable (f ∘ Subtype.val)<GOAL>∑' (x : ↑(s ∪ t)), f ↑x = ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>T2Space α<VAR>ContinuousMul α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>t : ι → Set β<VAR>hd : (↑s).Pairwise (Disjoint on t)<VAR>hf : ∀ i ∈ s, Multipliable (f ∘ Subtype.val)<GOAL>∏' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∏ i ∈ s, ∏' (x : ↑(t i)), f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>T2Space α<VAR>ContinuousAdd α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>t : ι → Set β<VAR>hd : (↑s).Pairwise (Disjoint on t)<VAR>hf : ∀ i ∈ s, Summable (f ∘ Subtype.val)<GOAL>∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>NormedField 𝕜<VAR>AddCommGroup H<VAR>Module 𝕜 H<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace H<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>FunLike hom H (α → E)<VAR>LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑UniformFun.ofFun ∘ ⇑φ)<VAR>h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>NormedField 𝕜<VAR>AddCommGroup H<VAR>Module 𝕜 H<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace H<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>FunLike hom H (α → E)<VAR>LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ ⇑φ)<VAR>h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>H : Submodule 𝕜 (α →ᵤ[𝔖] E)<VAR>h : ∀ u ∈ H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (u '' s)<GOAL>ContinuousSMul 𝕜 ↥H
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>V W : CategoryTheory.Pairwise ι<VAR>i : V ⟶ W<GOAL>(TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U).map i = TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverMap U i
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>∀ (a : CategoryTheory.Pairwise ι), (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U).obj a = TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj U a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheaf ↔ F.IsSheafPairwiseIntersections
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<GOAL>(F.interUnionPullbackCone U V).pt = F.val.obj (Opposite.op (U ⊔ V))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<GOAL>(F.interUnionPullbackCone U V).fst = F.val.map (CategoryTheory.homOfLE ⋯).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<GOAL>(F.interUnionPullbackCone U V).snd = F.val.map (CategoryTheory.homOfLE ⋯).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<VAR>s : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).op)<GOAL>F.interUnionPullbackConeLift U V s ≫ F.val.map (CategoryTheory.homOfLE ⋯).op = s.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<VAR>s : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).op)<GOAL>F.interUnionPullbackConeLift U V s ≫ F.val.map (CategoryTheory.homOfLE ⋯).op = s.snd
<VAR>X : TopCat<VAR>F : TopCat.Sheaf CommRingCat X<VAR>U V : TopologicalSpace.Opens ↑X<VAR>x : ↑(F.val.obj (Opposite.op (U ⊔ V)))<GOAL>(↑((F.objSupIsoProdEqLocus U V).hom x)).1 = (F.val.map (CategoryTheory.homOfLE ⋯).op) x
<VAR>X : TopCat<VAR>F : TopCat.Sheaf CommRingCat X<VAR>U V : TopologicalSpace.Opens ↑X<VAR>x : ↑(F.val.obj (Opposite.op (U ⊔ V)))<GOAL>(↑((F.objSupIsoProdEqLocus U V).hom x)).2 = (F.val.map (CategoryTheory.homOfLE ⋯).op) x
<VAR>X : TopCat<VAR>F : TopCat.Sheaf CommRingCat X<VAR>U V : TopologicalSpace.Opens ↑X<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)))))<GOAL>(F.val.map (CategoryTheory.homOfLE ⋯).op) ((F.objSupIsoProdEqLocus U V).inv x) = (↑x).1
<VAR>X : TopCat<VAR>F : TopCat.Sheaf CommRingCat X<VAR>U V : TopologicalSpace.Opens ↑X<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)))))<GOAL>(F.val.map (CategoryTheory.homOfLE ⋯).op) ((F.objSupIsoProdEqLocus U V).inv x) = (↑x).2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂<GOAL>Embedding ⇑(StarSubalgebra.inclusion h)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂<VAR>hS₁ : IsClosed ↑S₁<GOAL>ClosedEmbedding ⇑(StarSubalgebra.inclusion h)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>s : StarSubalgebra R A<GOAL>s.topologicalClosure.toSubalgebra = s.topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>s : StarSubalgebra R A<GOAL>↑s.topologicalClosure = closure ↑s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>s : StarSubalgebra R A<GOAL>s ≤ s.topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>s : StarSubalgebra R A<GOAL>IsClosed ↑s.topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>s t : StarSubalgebra R A<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<GOAL>Monotone StarSubalgebra.topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>TopologicalSpace B<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>TopologicalSemiring B<VAR>ContinuousStar B<VAR>s : StarSubalgebra R A<VAR>φ : A →⋆ₐ[R] B<VAR>hφ : IsClosedMap ⇑φ<GOAL>(StarSubalgebra.map φ s).topologicalClosure ≤ StarSubalgebra.map φ s.topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>TopologicalSpace B<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>TopologicalSemiring B<VAR>ContinuousStar B<VAR>s : StarSubalgebra R A<VAR>φ : A →⋆ₐ[R] B<VAR>hφ : Continuous ⇑φ<GOAL>StarSubalgebra.map φ s.topologicalClosure ≤ (StarSubalgebra.map φ s).topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>TopologicalSpace B<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>TopologicalSemiring B<VAR>ContinuousStar B<VAR>s : StarSubalgebra R A<VAR>φ : A →⋆ₐ[R] B<VAR>hφ : ClosedEmbedding ⇑φ<GOAL>(StarSubalgebra.map φ s).topologicalClosure = StarSubalgebra.map φ s.topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>s : Subalgebra R A<GOAL>(star s).topologicalClosure = star s.topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>TopologicalSpace B<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>T2Space B<VAR>S : StarSubalgebra R A<VAR>φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ.comp (StarSubalgebra.inclusion ⋯) = ψ.comp (StarSubalgebra.inclusion ⋯)<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>TopologicalSpace B<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>T2Space B<VAR>F : Type u_4<VAR>S : StarSubalgebra R A<VAR>FunLike F (↥S.topologicalClosure) B<VAR>AlgHomClass F R (↥S.topologicalClosure) B<VAR>StarAlgHomClass F R (↥S.topologicalClosure) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : ∀ (x : ↥S), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x)<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>StarRing A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>Algebra R A<VAR>StarModule R A<VAR>x : A<GOAL>x ∈ elementalStarAlgebra R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>StarRing A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>Algebra R A<VAR>StarModule R A<VAR>x : A<GOAL>star x ∈ elementalStarAlgebra R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>StarRing A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>Algebra R A<VAR>StarModule R A<VAR>x : A<GOAL>IsClosed ↑(elementalStarAlgebra R x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>StarRing A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>hx : x ∈ S<GOAL>elementalStarAlgebra R x ≤ S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>StarRing A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>Algebra R A<VAR>StarModule R A<VAR>x : A<GOAL>ClosedEmbedding Subtype.val
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>StarRing A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>Algebra R A<VAR>StarModule R A<VAR>x y : A<VAR>hy : y ∈ elementalStarAlgebra R x<VAR>P : (u : A) → u ∈ elementalStarAlgebra R x → Prop<VAR>self : P x ⋯<VAR>star_self : P (star x) ⋯<VAR>algebraMap : ∀ (r : R), P ((algebraMap R A) r) ⋯<VAR>add : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u + v) ⋯<VAR>mul : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u * v) ⋯<VAR>closure : ∀ (s : Set A) (hs : s ⊆ ↑(elementalStarAlgebra R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure s), P v ⋯<GOAL>P y hy
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSpace A<VAR>Semiring A<VAR>StarRing A<VAR>TopologicalSemiring A<VAR>ContinuousStar A<VAR>Algebra R A<VAR>StarModule R A<VAR>TopologicalSpace B<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>T2Space B<VAR>F : Type u_4<VAR>a : A<VAR>FunLike F (↥(elementalStarAlgebra R a)) B<VAR>AlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>AddCommMonoid A<VAR>StarAddMonoid A<VAR>Module R A<VAR>StarModule R A<VAR>TopologicalSpace A<VAR>ContinuousStar A<GOAL>∀ (a : A), (starL R) a = star a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>AddCommMonoid A<VAR>StarAddMonoid A<VAR>Module R A<VAR>StarModule R A<VAR>TopologicalSpace A<VAR>ContinuousStar A<GOAL>∀ (a : A), (starL R).symm a = starAddEquiv.symm a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TrivialStar R<VAR>AddCommMonoid A<VAR>StarAddMonoid A<VAR>Module R A<VAR>StarModule R A<VAR>TopologicalSpace A<VAR>ContinuousStar A<GOAL>∀ (a : A), (starL' R).symm a = (starL R).symm ({ toFun := id, map_add' := ⋯, map_smul' := ⋯, invFun := id, left_inv := ⋯, right_inv := ⋯ }.symm a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>TrivialStar R<VAR>AddCommMonoid A<VAR>StarAddMonoid A<VAR>Module R A<VAR>StarModule R A<VAR>TopologicalSpace A<VAR>ContinuousStar A<GOAL>∀ (a : A), (starL' R) a = star a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>TopologicalSpace A<VAR>ContinuousAdd A<VAR>ContinuousStar A<VAR>ContinuousConstSMul R A<GOAL>Continuous ⇑(selfAdjointPart R)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>TopologicalSpace A<VAR>ContinuousSub A<VAR>ContinuousStar A<VAR>ContinuousConstSMul R A<GOAL>Continuous ⇑(skewAdjointPart R)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>TopologicalSpace A<VAR>TopologicalAddGroup A<VAR>ContinuousStar A<VAR>ContinuousConstSMul R A<GOAL>Continuous ⇑(StarModule.decomposeProdAdjoint R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>TopologicalSpace A<VAR>TopologicalAddGroup A<GOAL>Continuous ⇑(StarModule.decomposeProdAdjoint R A).symm
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>TopologicalSpace A<VAR>ContinuousAdd A<VAR>ContinuousStar A<VAR>ContinuousConstSMul R A<VAR>x : A<GOAL>↑((selfAdjointPartL R A) x) = ⅟2 • x + ⅟2 • star x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>TopologicalSpace A<VAR>ContinuousSub A<VAR>ContinuousStar A<VAR>ContinuousConstSMul R A<VAR>x : A<GOAL>↑((skewAdjointPartL R A) x) = ⅟2 • (x - star x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>TopologicalSpace A<VAR>TopologicalAddGroup A<VAR>ContinuousStar A<VAR>ContinuousConstSMul R A<VAR>a : ↥(selfAdjoint A) × ↥(skewAdjoint A)<GOAL>(StarModule.decomposeProdAdjointL R A).symm a = (selfAdjoint.submodule R A).subtype a.1 + (skewAdjoint.submodule R A).subtype a.2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>TopologicalSpace A<VAR>TopologicalAddGroup A<VAR>ContinuousStar A<VAR>ContinuousConstSMul R A<VAR>i : A<GOAL>(StarModule.decomposeProdAdjointL R A) i = ((selfAdjointPart R) i, (skewAdjointPart R) i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>self : LocallyConvexSpace 𝕜 E<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ Convex 𝕜 s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<GOAL>LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ Convex 𝕜 s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ι : Type u_3<VAR>b : E → ι → Set E<VAR>p : E → ι → Prop<VAR>hbasis : ∀ (x : E), (𝓝 x).HasBasis (p x) (b x)<VAR>hconvex : ∀ (x : E) (i : ι), p x i → Convex 𝕜 (b x i)<GOAL>LocallyConvexSpace 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>LocallyConvexSpace 𝕜 E<GOAL>(𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ Convex 𝕜 s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<GOAL>LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), ∀ U ∈ 𝓝 x, ∃ S ∈ 𝓝 x, Convex 𝕜 S ∧ S ⊆ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ι : Type u_3<VAR>b : ι → Set E<VAR>p : ι → Prop<VAR>hbasis : (𝓝 0).HasBasis p b<VAR>hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)<GOAL>LocallyConvexSpace 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<GOAL>LocallyConvexSpace 𝕜 E ↔ (𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ Convex 𝕜 s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<GOAL>LocallyConvexSpace 𝕜 E ↔ ∀ U ∈ 𝓝 0, ∃ S ∈ 𝓝 0, Convex 𝕜 S ∧ S ⊆ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>LocallyConvexSpace 𝕜 E<GOAL>(𝓝 0).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>ts : Set (TopologicalSpace E)<VAR>h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E<GOAL>LocallyConvexSpace 𝕜 E
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>ts' : ι → TopologicalSpace E<VAR>h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E<GOAL>LocallyConvexSpace 𝕜 E
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>t₁ t₂ : TopologicalSpace E<VAR>h₁ : LocallyConvexSpace 𝕜 E<VAR>h₂ : LocallyConvexSpace 𝕜 E<GOAL>LocallyConvexSpace 𝕜 E
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>t : TopologicalSpace F<VAR>LocallyConvexSpace 𝕜 F<VAR>f : E →ₗ[𝕜] F<GOAL>LocallyConvexSpace 𝕜 E
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>self : NonarchimedeanAddGroup G<VAR>U : Set G<GOAL>U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>self : NonarchimedeanGroup G<VAR>U : Set G<GOAL>U ∈ 𝓝 1 → ∃ V, ↑V ⊆ U
<VAR>R : Type u_1<VAR>Ring R<VAR>TopologicalSpace R<VAR>self : NonarchimedeanRing R<VAR>U : Set R<GOAL>U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>NonarchimedeanAddGroup G<VAR>H : Type u_2<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>TopologicalAddGroup H<VAR>f : G →+ H<VAR>emb : OpenEmbedding ⇑f<GOAL>NonarchimedeanAddGroup H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>NonarchimedeanGroup G<VAR>H : Type u_2<VAR>Group H<VAR>TopologicalSpace H<VAR>TopologicalGroup H<VAR>f : G →* H<VAR>emb : OpenEmbedding ⇑f<GOAL>NonarchimedeanGroup H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>NonarchimedeanGroup G<VAR>K : Type u_3<VAR>Group K<VAR>TopologicalSpace K<VAR>NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>hU : U ∈ 𝓝 1<GOAL>∃ V W, ↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>NonarchimedeanAddGroup G<VAR>K : Type u_3<VAR>AddGroup K<VAR>TopologicalSpace K<VAR>NonarchimedeanAddGroup K<VAR>U : Set (G × K)<VAR>hU : U ∈ 𝓝 0<GOAL>∃ V W, ↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>NonarchimedeanGroup G<VAR>U : Set (G × G)<VAR>hU : U ∈ 𝓝 1<GOAL>∃ V, ↑V ×ˢ ↑V ⊆ U
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>NonarchimedeanAddGroup G<VAR>U : Set (G × G)<VAR>hU : U ∈ 𝓝 0<GOAL>∃ V, ↑V ×ˢ ↑V ⊆ U
<VAR>R : Type u_1<VAR>Ring R<VAR>TopologicalSpace R<VAR>NonarchimedeanRing R<VAR>U : OpenAddSubgroup R<VAR>r : R<GOAL>∃ V, r • ↑V ⊆ ↑U
<VAR>R : Type u_1<VAR>Ring R<VAR>TopologicalSpace R<VAR>NonarchimedeanRing R<VAR>U : OpenAddSubgroup R<GOAL>∃ V, ↑V * ↑V ⊆ ↑U
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>TopologicalSpace 𝕜<VAR>CommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<GOAL>Continuous fun x y => (B x) y