English
For any open subset s of X, the ideal of C(X, 𝕜) corresponding to s is maximal if and only if s is a coatom in the lattice of opens; equivalently, maximal ideals correspond to complements of singletons in the underlying space.
Русский
Для любого открытого s в X идеал C(X, 𝕜), соответствующий s, максимален тогда и только тогда, когда s является коатомой в решётке открытых множеств; эквивалентно максимумальные идеалы соответствуют дополнениям одиночных точек.
LaTeX
$$$\\big(\\mathrm{idealOfSet}\\, 𝕜\\,(s)\\big).\\mathrm{IsMaximal} \\iff \\mathrm{IsCoatom}(s).$$$
Lean4
theorem idealOfSet_isMaximal_iff (s : Opens X) : (idealOfSet 𝕜 (s : Set X)).IsMaximal ↔ IsCoatom s :=
by
rw [Ideal.isMaximal_def]
refine (idealOpensGI X 𝕜).isCoatom_iff (fun I hI => ?_) s
rw [← Ideal.isMaximal_def] at hI
exact idealOfSet_ofIdeal_isClosed inferInstance
