English
If φ and ψ are continuous and agree on the inclusion, then they are equal on the topological closure of the subalgebra.
Русский
Если два отображения непрерывны и совпадают на включении, то они совпадают на топологическом замыкании подалгебры.
LaTeX
$$StarAlgHom.ext_topologicalClosure$$
Lean4
theorem _root_.StarAlgHomClass.ext_topologicalClosure [T2Space B] {F : Type*} {S : StarSubalgebra R A}
[FunLike F S.topologicalClosure B] [AlgHomClass F R S.topologicalClosure B] [StarHomClass F S.topologicalClosure B]
{φ ψ : F} (hφ : Continuous φ) (hψ : Continuous ψ)
(h : ∀ x : S, φ (inclusion (le_topologicalClosure S) x) = ψ ((inclusion (le_topologicalClosure S)) x)) : φ = ψ :=
by
have : (φ : S.topologicalClosure →⋆ₐ[R] B) = (ψ : S.topologicalClosure →⋆ₐ[R] B) :=
by
refine StarAlgHom.ext_topologicalClosure (R := R) (A := A) (B := B) hφ hψ (StarAlgHom.ext ?_)
simpa only [StarAlgHom.coe_comp, StarAlgHom.coe_coe] using h
rw [DFunLike.ext'_iff, ← StarAlgHom.coe_coe]
apply congrArg _ this
