setOfIdeal_eq_compl_singleton — Mathlib

English

Every maximal ideal I of C(X, 𝕜) arises as the ideal of functions vanishing outside a single point; i.e., there exists x with setOfIdeal I = X \\ {x}.

Русский

Каждый максимальный идеал I в C(X, 𝕜) есть как множество функций, не обращённых вне одной точки; то есть существует x такой, что setOfIdeal I = X \\ {x}.

LaTeX

$$\\exists x: X,\\ setOfIdeal I = X \\ {x}$$

Lean4

theorem setOfIdeal_eq_compl_singleton (I : Ideal C(X, 𝕜)) [hI : I.IsMaximal] : ∃ x : X, setOfIdeal I = { x }ᶜ :=
  by
  have h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal :=
    (idealOfSet_ofIdeal_isClosed (inferInstance : IsClosed (I : Set C(X, 𝕜)))).symm ▸ hI
  obtain ⟨x, hx⟩ := Opens.isCoatom_iff.1 ((idealOfSet_isMaximal_iff 𝕜 (opensOfIdeal I)).1 h)
  exact ⟨x, congr_arg (fun (s : Opens X) => (s : Set X)) hx⟩

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