zeroLocus_iSup — Mathlib

English

Let I be a family of ideals I_i in R. The zero locus of the sup (i.e., the smallest ideal containing all I_i) equals the intersection of the zero loci:

Русский

Пусть I_i — семейство идеалов в R. Нулевой локус верхатипного объединения равен пересечению нулевых локусов:

LaTeX

$$$\\mathrm{zeroLocus}\\left(\\big(\\sup_i I_i\\big) : \\{R\\} \\right) = \\bigcap_i \\mathrm{zeroLocus}(I_i).$$$

Lean4

theorem zeroLocus_iSup {ι : Sort*} (I : ι → Ideal R) :
    zeroLocus ((⨆ i, I i : Ideal R) : Set R) = ⋂ i, zeroLocus (I i) :=
  (gc R).l_iSup

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