mem_compl_zeroLocus_iff_notMem — Mathlib

English

For any f in R and I in PrimeSpectrum(R), I is in the complement of zeroLocus({f}) exactly when f is not in the ideal of I:

Русский

Для любого f в R и I в PrimeSpectrum(R) член I принадлежит дополнению нулевого локуса {f} тогда и только тогда, когда f не принадлежит аидеалу I:

LaTeX

$$$I \\in (\\mathrm{zeroLocus} \\{f\\})^{c} \\iff f \\notin I.asIdeal.$$$

Lean4

theorem mem_compl_zeroLocus_iff_notMem {f : R} {I : PrimeSpectrum R} :
    I ∈ (zeroLocus { f } : Set (PrimeSpectrum R))ᶜ ↔ f ∉ I.asIdeal := by
  rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]; rfl

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