zeroLocus_iUnion — Mathlib

English

Let s be a family of subsets s_i of R. The zero locus of the union across i equals the intersection of the zero loci:

Русский

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

LaTeX

$$$\\mathrm{zeroLocus}\\left(\\bigcup_i s_i\\right) = \\bigcap_i \\mathrm{zeroLocus}(s_i).$$$

Lean4

theorem zeroLocus_iUnion {ι : Sort*} (s : ι → Set R) : zeroLocus (⋃ i, s i) = ⋂ i, zeroLocus (s i) :=
  (gc_set R).l_iSup

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