English
If two star-alg homomorphisms f,g from adjoin_R({a}) agree on a in A, then f = g.
Русский
Если две звездно-алгебра-хомоморфизма f,g из adjoin_R({a}) совпадают на элементе a ∈ A, то f = g.
LaTeX
$$$ f\\langle a, \\mathrm{self\_mem\\_adjoin\\_singleton}\\rangle = g\\langle a, \\mathrm{self\_mem\\_adjoin\\_singleton}\\rangle \\Rightarrow f = g $$$
Lean4
theorem ext_adjoin_singleton {a : A} [FunLike F (adjoin R ({ a } : Set A)) B]
[AlgHomClass F R (adjoin R ({ a } : Set A)) B] [StarHomClass F (adjoin R ({ a } : Set A)) B] {f g : F}
(h : f ⟨a, self_mem_adjoin_singleton R a⟩ = g ⟨a, self_mem_adjoin_singleton R a⟩) : f = g :=
ext_adjoin fun x hx =>
(show x = ⟨a, self_mem_adjoin_singleton R a⟩ from Subtype.ext <| Set.mem_singleton_iff.mp hx).symm ▸ h
