isClosed_iff_zeroLocus — Mathlib

English

A subset Z of the prime spectrum is closed if and only if Z is the zero locus of some ideal of R.

Русский

Подмножество Z множества спектра замкнуто тогда и только тогда, когда Z есть нулевая локус некоего идеала кольца R.

LaTeX

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

Lean4

theorem isClosed_iff_zeroLocus (Z : Set (PrimeSpectrum R)) : IsClosed Z ↔ ∃ s, Z = zeroLocus s := by
  rw [← isOpen_compl_iff, isOpen_iff, compl_compl]

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