Theorems · Theorem · functional analysis

StarSubalgebra.topologicalClosure_map

∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A]
  [inst_6 : StarModule R A] [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A]
  [inst_9 : TopologicalSpace B] [inst_10 : Semiring B] [inst_11 : Algebra R B] [inst_12 : StarRing B]
  [inst_13 : StarModule R B] [inst_14 : IsSemitopologicalSemiring B] [inst_15 : ContinuousStar B]
  (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B),
  IsClosedMap ⇑φ →
    Continuous ⇑φ → (StarSubalgebra.map φ s).topologicalClosure = StarSubalgebra.map φ s.topologicalClosure

Defined in

Mathlib.Topology.Algebra.StarSubalgebra

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringStarRingTopologicalSpaceSemiringAlgebraStarRingStarModuleIsSemitopologicalSemiringContinuousStarTopologicalSpaceSemiringAlgebraStarRingStarModuleIsSemitopologicalSemiringContinuousStar