supportSet_inter — Mathlib

English

For any I and affine open U, the intersection of the support with U equals the intersection of the zero locus with U.

Русский

Для любого I и аффинного открытого U пересечение поддержки с U равно пересечению нулевой локусы с U.

LaTeX

$$$I.supportSet \cap U = X.zeroLocus(I.ideal U) \cap U$$$

Lean4

theorem supportSet_inter (I : IdealSheafData X) (U : X.affineOpens) :
    I.supportSet ∩ U = X.zeroLocus (U := U.1) (I.ideal U) ∩ U :=
  by
  ext x
  by_cases hxU : x ∈ U.1
  · simp [hxU, mem_supportSet_iff_of_mem hxU]
  · simp [hxU]

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