basicOpen_eq_zeroLocus_compl — Mathlib

English

The basic open set for r is the complement of the primes containing r; equivalently, it is the complement of the zero locus of r.

Русский

Базисное открытое множество для r является дополнением к нулевой локусе элемента r.

LaTeX

$$$$ \\mathrm{basicOpen}(r) = (\\mathrm{zeroLocus}(\\{r\\}))^{\\complement}. $$$$

Lean4

@[simp]
theorem basicOpen_eq_zeroLocus_compl (r : R) : (basicOpen r : Set (PrimeSpectrum R)) = (zeroLocus { r })ᶜ :=
  Set.ext fun x => by
    simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]

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