ideal_gc — Mathlib

English

For any ideal I and x ∈ X, x ∈ setOfIdeal(I) iff there exists f ∈ I with f(x) ≠ 0.

Русский

Для идеала I и точки x существование f ∈ I с f(x) ≠ 0 эквивалентно x ∈ setOfIdeal(I).

LaTeX

$$$ x \\in setOfIdeal(I) \\iff \\exists f \\in I, f(x) \\neq 0 $$$

Lean4

theorem ideal_gc : GaloisConnection (setOfIdeal : Ideal C(X, R) → Set X) (idealOfSet R) :=
  by
  refine fun I s => ⟨fun h f hf => ?_, fun h x hx => ?_⟩
  · by_contra h'
    rcases notMem_idealOfSet.mp h' with ⟨x, hx, hfx⟩
    exact hfx (notMem_setOfIdeal.mp (mt (@h x) hx) hf)
  · obtain ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
    by_contra hx'
    exact notMem_idealOfSet.mpr ⟨x, hx', hfx⟩ (h hf)

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