idealOf_compl_singleton_isMaximal

English

For every point x in X, the ideal of C(X, 𝕜) associated with the complement of {x} is a maximal ideal.

Русский

Для каждой точки x пространства X соответствующий идеал в C(X, 𝕜), связанный с дополнением к единичному множества {x}, является максимальным идеалом.

LaTeX

$$(idealOfSet 𝕜 ({x}^c)).IsMaximal$$

Lean4

theorem idealOf_compl_singleton_isMaximal (x : X) : (idealOfSet 𝕜 ({ x }ᶜ : Set X)).IsMaximal :=
  (idealOfSet_isMaximal_iff 𝕜 (Closeds.singleton x).compl).mpr <| Opens.isCoatom_iff.mpr ⟨x, rfl⟩

Похожие утверждения