zeroLocus_iUnion₂ — Mathlib

English

For a two-parameter family s_i_j of subsets, the zero locus of the union over i and j equals the intersection over i and j of the zero loci:

Русский

Для семейства s_{i,j} двусвязной размерности нулевой локус объединения по i и j равен пересечению нулевых локусов по всем i, j:

LaTeX

$$$\\mathrm{zeroLocus}\\left(\\bigcup_i \\bigcup_j s_{i j}\\right) = \\bigcap_i \\bigcap_j \\mathrm{zeroLocus}(s_{i j}).$$$

Lean4

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

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