English
Given a uniform space A and a StarSubalgebra S, the topologicalClosure of S forms a complete space when viewed as a subtype.
Русский
Пусть A — униформное пространство и S —StarSubalgebra; topologicalClosure(S) образует полноразмерное пространство как подмножество.
LaTeX
$$CompleteSpace (S.topologicalClosure)$$
Lean4
/-- Continuous `StarAlgHom`s from the topological closure of a `StarSubalgebra` whose
compositions with the `StarSubalgebra.inclusion` map agree are, in fact, equal. -/
theorem _root_.StarAlgHom.ext_topologicalClosure [T2Space B] {S : StarSubalgebra R A}
{φ ψ : S.topologicalClosure →⋆ₐ[R] B} (hφ : Continuous φ) (hψ : Continuous ψ)
(h : φ.comp (inclusion (le_topologicalClosure S)) = ψ.comp (inclusion (le_topologicalClosure S))) : φ = ψ :=
by
rw [DFunLike.ext'_iff]
have : DenseRange (Set.inclusion (le_topologicalClosure S)) := by simp [-SetLike.coe_sort_coe]
refine Continuous.ext_on this hφ hψ ?_
rintro _ ⟨x, rfl⟩
simpa only using DFunLike.congr_fun h x
