basicOpen_eq_zeroLocus_compl — Mathlib

English

The basic open set is the complement of the zero locus of the singleton { r }.

Русский

Множество basicOpen 𝒜 r является дополнением нулевого множества единичного множества { r }.

LaTeX

$$$ (\mathrm{basicOpen}_{\mathcal{A}}(r)) = (\mathrm{zeroLocus}_{\mathcal{A}}({r}))^{\mathsf{c}} $$$

Lean4

@[simp]
theorem basicOpen_eq_zeroLocus_compl (r : A) : (basicOpen 𝒜 r : Set (ProjectiveSpectrum 𝒜)) = (zeroLocus 𝒜 { r })ᶜ :=
  Set.ext fun x => by simp only [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]; rfl

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