mem_support_iff — Mathlib

English

For any x, x is in the support of I iff x is in the zero locus of I on every affine open containing x.

Русский

Для каждого x, x принадлежит поддержке I тогда и только тогда, когда x лежит в нулевой локусе I на каждом аффинном открытии, содержащем x.

LaTeX

$$x ∈ I.support ↔ ∀ U, x ∈ X.zeroLocus(I.ideal U)$$

Lean4

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

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