coe_support_inter — Mathlib

English

The intersection of the support set with an affine open equals the intersection of the zero locus with that open.

Русский

Пересечение поддержки с аффинным открытым равно пересечению нулевой локусы с этим открытым.

LaTeX

$$(I.support : Set X) ∩ U = X.zeroLocus(I.ideal U) ∩ U$$

Lean4

theorem coe_support_inter (I : IdealSheafData X) (U : X.affineOpens) :
    (I.support : Set X) ∩ U = X.zeroLocus (U := U.1) (I.ideal U) ∩ U :=
  I.supportSet_inter U

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