biUnion_finsetSigma_univ — Mathlib

English

For a finite index set s and a family f: Sigma κ → Set α, the double union over the sigma-index equals the iterated union over i in s and j.

Русский

Для конечного множества индексов s и семейства f: Sigma κ → Set α сумма по сигма-индексам эквивалентна попарному объединению по i в s и по j.

LaTeX

$$$\bigcup_{(i,j)\in s.\sigma} f(i,j) = \bigcup_{i\in s} \bigcup_j f(i,j)$$$

Lean4

theorem biUnion_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
    ⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩ := by aesop

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