zeroLocus_iUnion — Mathlib

English

For any family of open sets f i in Γ(X, U), the zero locus of the union equals the intersection of the zero loci: zeroLocus(⋃ i, f i) = ⋂ i, zeroLocus(f i).

Русский

Для семейства множеств открытых f_i в Γ(X, U) нулевая область объединения равна пересечению нулевых областей: zeroLocus(⋃ i, f i) = ⋂ i, zeroLocus(f i).

LaTeX

$$$X.zeroLocus(\bigcup_i f_i) = \bigcap_i X.zeroLocus(f_i)$$$

Lean4

theorem zeroLocus_iUnion {U : X.Opens} {ι : Type*} (f : ι → Set Γ(X, U)) :
    X.zeroLocus (⋃ i, f i) = ⋂ i, X.zeroLocus (f i) := by
  simpa [zeroLocus, AlgebraicGeometry.RingedSpace.zeroLocus] using Set.iInter_comm _

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