mem_supportSet_iff — Mathlib

English

For any I and x on X, x lies in I.supportSet iff x lies in every zero locus Z(I(U)) across all affine opens U.

Русский

Для любого I и точки x на X: x ∈ supportSet(I) тогда и только тогда, когда x ∈ Z(I(U)) для всех аффинных открытых U.

LaTeX

$$$x \in I.supportSet \iff \forall U, x \in X.zeroLocus(U)(I.ideal U)$$$

Lean4

theorem mem_supportSet_iff {I : IdealSheafData X} {x} :
    x ∈ I.supportSet ↔ ∀ U, x ∈ X.zeroLocus (U := U.1) (I.ideal U) :=
  (Set.ext_iff.mp I.supportSet_eq_iInter_zeroLocus _).trans Set.mem_iInter

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