zeroLocus_bUnion — Mathlib

English

Let s be a set of subsets of R. The zero locus of the union of all members of s equals the intersection over members of s of their zero loci:

Русский

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

LaTeX

$$$\\mathrm{zeroLocus}\\left(\\bigcup s' \\in s, s' : \\mathrm{Set} R\\right) = \\bigcap_{s'\\in s} \\mathrm{zeroLocus}(s').$$$

Lean4

theorem zeroLocus_bUnion (s : Set (Set R)) : zeroLocus (⋃ s' ∈ s, s' : Set R) = ⋂ s' ∈ s, zeroLocus s' := by
  simp only [zeroLocus_iUnion]

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