English
Under natural mild hypotheses on 𝕜, the character space is a closed subset of the WeakDual space of A with values in 𝕜.
Русский
При естественных мягких предположениях на 𝕜 множество характеров является замкнутым подмножеством слабого двойственного пространства A → 𝕜.
LaTeX
$$$\operatorname{Char}_{\mathbb{k}}(A) \text{ is a closed subset of } \mathrm{WeakDual}_{\mathbb{k}}(A).$$$
Lean4
/-- under suitable mild assumptions on `𝕜`, the character space is a closed set in
`WeakDual 𝕜 A`. -/
protected theorem isClosed [Nontrivial 𝕜] [T2Space 𝕜] [ContinuousMul 𝕜] : IsClosed (characterSpace 𝕜 A) :=
by
rw [eq_set_map_one_map_mul, Set.setOf_and]
refine IsClosed.inter (isClosed_eq (eval_continuous _) continuous_const) ?_
simpa only [(union_zero 𝕜 A).symm] using union_zero_isClosed _ _
