missing lemmas about topological star algebras

theorem Set.isClosed_centralizer {M : Type u_1} (s : Set M) [Mul M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] : IsClosed s.centralizer

theorem NonUnitalStarAlgHom.range_eq_map_top {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarRing A] [StarModule R A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (φ : F) : NonUnitalStarAlgHom.range φ = NonUnitalStarSubalgebra.map φ ⊤

theorem StarAlgebra.topologicalClosure_adjoin_le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousStar A] [T2Space A] (s : Set A) : (adjoin R s).topologicalClosure ≤ StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R s)

theorem StarAlgebra.elemental.le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousStar A] [T2Space A] (x : A) : elemental R x ≤ StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R {x})

theorem NonUnitalSubalgebra.map_topologicalClosure_le {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [TopologicalSpace A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [TopologicalSpace B] [NonUnitalSemiring B] [Module R B] [IsTopologicalSemiring B] [ContinuousConstSMul R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (s : NonUnitalSubalgebra R A) (φ : F) (hφ : Continuous ⇑φ) : map φ s.topologicalClosure ≤ (map φ s).topologicalClosure

theorem NonUnitalSubalgebra.topologicalClosure_map_le {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [TopologicalSpace A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [TopologicalSpace B] [NonUnitalSemiring B] [Module R B] [IsTopologicalSemiring B] [ContinuousConstSMul R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (s : NonUnitalSubalgebra R A) (φ : F) (hφ : IsClosedMap ⇑φ) : (map φ s).topologicalClosure ≤ map φ s.topologicalClosure

theorem NonUnitalSubalgebra.topologicalClosure_map {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [TopologicalSpace A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [TopologicalSpace B] [NonUnitalSemiring B] [Module R B] [IsTopologicalSemiring B] [ContinuousConstSMul R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (s : NonUnitalSubalgebra R A) (φ : F) (hφ : Topology.IsClosedEmbedding ⇑φ) : (map φ s).topologicalClosure = map φ s.topologicalClosure

theorem NonUnitalStarSubalgebra.map_topologicalClosure_le {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] [TopologicalSpace B] [Star B] [NonUnitalSemiring B] [Module R B] [IsTopologicalSemiring B] [ContinuousConstSMul R B] [ContinuousStar B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (s : NonUnitalStarSubalgebra R A) (φ : F) (hφ : Continuous ⇑φ) : map φ s.topologicalClosure ≤ (map φ s).topologicalClosure

theorem NonUnitalStarSubalgebra.topologicalClosure_map_le {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] [TopologicalSpace B] [Star B] [NonUnitalSemiring B] [Module R B] [IsTopologicalSemiring B] [ContinuousConstSMul R B] [ContinuousStar B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (s : NonUnitalStarSubalgebra R A) (φ : F) (hφ : IsClosedMap ⇑φ) : (map φ s).topologicalClosure ≤ map φ s.topologicalClosure

theorem NonUnitalStarSubalgebra.topologicalClosure_map {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] [TopologicalSpace B] [Star B] [NonUnitalSemiring B] [Module R B] [IsTopologicalSemiring B] [ContinuousConstSMul R B] [ContinuousStar B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (s : NonUnitalStarSubalgebra R A) (φ : F) (hφ : Topology.IsClosedEmbedding ⇑φ) : (map φ s).topologicalClosure = map φ s.topologicalClosure

theorem NonUnitalStarAlgebra.topologicalClosure_adjoin_le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarRing A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousStar A] [T2Space A] [ContinuousConstSMul R A] (s : Set A) : (adjoin R s).topologicalClosure ≤ NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R s)

theorem NonUnitalStarAlgebra.elemental.le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarRing A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousStar A] [T2Space A] [ContinuousConstSMul R A] (x : A) : elemental R x ≤ NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R {x})