supportSet_subset_zeroLocus — Mathlib

English

For any I and affine open U, the support set of I is contained in the zero locus Z(I(U)).

Русский

Для любого I и аффинного открытого U, supportSet(I) ⊆ Z(I(U)).

LaTeX

$$$ I.supportSet \subseteq X.zeroLocus (U := U.1) (I.ideal U) $$$

Lean4

theorem supportSet_subset_zeroLocus (I : IdealSheafData X) (U : X.affineOpens) :
    I.supportSet ⊆ X.zeroLocus (U := U.1) (I.ideal U) :=
  I.supportSet_eq_iInter_zeroLocus.trans_subset (Set.iInter_subset _ _)

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