isOpen_iff — Mathlib

English

An open subset U of the projective spectrum is open if and only if there exists a subset S of A such that U's complement is the vanishing locus of S.

Русский

Открытость U подпространства спектра эквивалентна существованию множества S ⊆ A, такого что дополнение U равно нулевой локус S.

LaTeX

$$$ \operatorname{IsOpen}(U) \iff \exists S, U^{c} = \operatorname{zeroLocus}_{\mathcal{A}}(S) $$$

Lean4

theorem isOpen_iff (U : Set (ProjectiveSpectrum 𝒜)) : IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s := by
  simp only [@eq_comm _ Uᶜ]; rfl

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