ideal_isMaximal_iff — Mathlib

English

For a maximal ideal I of C(X, 𝕜) that is closed (as a subset), there exists x ∈ X such that idealOfSet 𝕜 {x}^c = I.

Русский

Для максимального идеала I в C(X, 𝕜), который замкнут как множество, существует x ∈ X с равенством idealOfSet 𝕜 {x}^c = I.

LaTeX

$$\\exists x: X, idealOfSet 𝕜 \\{x\\}^c = I$$

Lean4

theorem ideal_isMaximal_iff (I : Ideal C(X, 𝕜)) [hI : IsClosed (I : Set C(X, 𝕜))] :
    I.IsMaximal ↔ ∃ x : X, idealOfSet 𝕜 { x }ᶜ = I :=
  by
  refine
    ⟨?_, fun h =>
      let ⟨x, hx⟩ := h
      hx ▸ idealOf_compl_singleton_isMaximal 𝕜 x⟩
  intro hI'
  obtain ⟨x, hx⟩ := setOfIdeal_eq_compl_singleton I
  exact
    ⟨x, by
      simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using congr_arg (idealOfSet 𝕜) hx.symm⟩

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