isClosed_iff_zeroLocus_ideal — Mathlib

English

A subset Z is closed if and only if there exists an ideal I with Z = zeroLocus I.

Русский

Замкнутость Z эквивалентна существованию идеала I с Z = zeroLocus(I).

LaTeX

$$$\\operatorname{IsClosed}(Z) \\iff \\exists I, Z = \\operatorname{zeroLocus}(I)$$$

Lean4

theorem isClosed_iff_zeroLocus_ideal (Z : Set (PrimeSpectrum R)) : IsClosed Z ↔ ∃ I : Ideal R, Z = zeroLocus I :=
  (isClosed_iff_zeroLocus _).trans ⟨fun ⟨s, hs⟩ => ⟨_, (zeroLocus_span s).substr hs⟩, fun ⟨I, hI⟩ => ⟨I, hI⟩⟩

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