Theorems · Theorem · functional analysis

StarAlgebra.elemental.starAlgHomClass_ext

∀ (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 : StarRing A] [inst_5 : IsSemitopologicalSemiring A]
  [inst_6 : ContinuousStar A] [inst_7 : Algebra R A] [inst_8 : StarModule R A] [inst_9 : TopologicalSpace B]
  [inst_10 : Semiring B] [inst_11 : StarRing B] [inst_12 : Algebra R B] [T2Space B] {F : Type u_4} {a : A}
  [inst_14 : FunLike F (↥(StarAlgebra.elemental R a)) B] [AlgHomClass F R (↥(StarAlgebra.elemental R a)) B]
  [StarHomClass F (↥(StarAlgebra.elemental R a)) B] {φ ψ : F},
  Continuous ⇑φ → Continuous ⇑ψ → φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩ → φ = ψ

Defined in

Mathlib.Topology.Algebra.StarSubalgebra

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingTopologicalSpaceSemiringStarRingIsSemitopologicalSemiringContinuousStarAlgebraStarModuleTopologicalSpaceSemiringStarRingAlgebraT2SpaceFunLikeAlgHomClassStarHomClass