Theorems · Theorem · functional analysis

StarAlgHomClass.ext_topologicalClosure

∀ {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] [T2Space B]
  {F : Type u_4} {S : StarSubalgebra R A} [inst_14 : FunLike F (↥S.topologicalClosure) B]
  [AlgHomClass F R (↥S.topologicalClosure) B] [StarHomClass F (↥S.topologicalClosure) B] {φ ψ : F},
  Continuous ⇑φ →
    Continuous ⇑ψ → (∀ (x : ↥S), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x)) → φ = ψ

Defined in

Mathlib.Topology.Algebra.StarSubalgebra

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingTopologicalSpaceSemiringAlgebraStarRingStarModuleIsSemitopologicalSemiringContinuousStarTopologicalSpaceSemiringAlgebraStarRingT2SpaceFunLikeAlgHomClassStarHomClass