missing lemmas about topological star algebras

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 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