mem_zeroLocus — Mathlib

English

For any x and s, x belongs to zeroLocus 𝒜 s if and only if s is contained in x.asHomogeneousIdeal.

Русский

Для любых x и s верно: x принадлежит zeroLocus 𝒜 s тогда и только тогда, когда s ⊆ x.asHomogeneousIdeal.

LaTeX

$$$$ x \\in \\mathrm{zeroLocus}(\\mathcal{A}, s) \\iff s \\subseteq x.asHomogeneousIdeal $$$$

Lean4

@[simp]
theorem mem_zeroLocus (x : ProjectiveSpectrum 𝒜) (s : Set A) : x ∈ zeroLocus 𝒜 s ↔ s ⊆ x.asHomogeneousIdeal :=
  Iff.rfl

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