zeroLocus_iUnion — Mathlib

English

For a family s_i of subsets of A, the vanishing locus of the union equals the intersection of the vanishing loci.

Русский

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

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}\left(\bigcup_i s_i\right) = \bigcap_i \operatorname{zeroLocus}_{\mathcal{A}}(s_i) $$$

Lean4

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

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