isClosed_iff_zeroLocus — Mathlib

English

A subset Z of the projective spectrum is closed if and only if there exists a subset S of A such that Z equals the vanishing locus of S.

Русский

Множество Z проективного спектра замкнуто тогда и только тогда, когда существует подмножество S ⊆ A, такое что Z равно нуль-множество S.

LaTeX

$$$ \operatorname{IsClosed}(Z) \iff \exists S, Z = \operatorname{zeroLocus}_{\mathcal{A}}(S) $$$

Lean4

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

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