English
If α is a subsingleton, then Subalgebra_R(C(α,R)) is a singleton; all continuous maps α→R are equal.
Русский
Если α — пододин, то Subalgebra_R(C(α,R)) является одиночной; все непрерывные отображения α→R совпадают.
LaTeX
$$$\\text{SubsingletonSubalgebra}(\\alpha) : \\text{Subsingleton}(\\mathrm{Subalgebra}(R, C(\\alpha,R))).$$$
Lean4
instance subsingleton_subalgebra (α : Type*) [TopologicalSpace α] (R : Type*) [CommSemiring R] [TopologicalSpace R]
[IsTopologicalSemiring R] [Subsingleton α] : Subsingleton (Subalgebra R C(α, R)) :=
⟨fun s₁ s₂ => by
cases isEmpty_or_nonempty α
· have : Subsingleton C(α, R) := DFunLike.coe_injective.subsingleton
subsingleton
· inhabit α
ext f
have h : f = algebraMap R C(α, R) (f default) := by
ext x'
simp only [mul_one, Algebra.id.smul_eq_mul, algebraMap_apply]
congr
simp [eq_iff_true_of_subsingleton]
rw [h]
simp only [Subalgebra.algebraMap_mem]⟩
