zeroLocus_bUnion — Mathlib

English

For a collection s of subsets of A indexed by a set, the zero locus of the union across the index s is the intersection across the index.

Русский

Для множества подмножеств, индексированного по множество, нуль-множество объединения равно пересечению нуль-множеств по индексу.

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}\left(\bigcup_{s' \in s} s'\right) = \bigcap_{s' \in s} \operatorname{zeroLocus}_{\mathcal{A}}(s') $$$

Lean4

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

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