biUnion_finsetSigma_univ' — Mathlib

English

With a family f: κ i → Set α, the same equality holds: union over i in s and j equals union over (i,j) in s.sigma.

Русский

С семейством f: κ i → Set α справедливо то же равенство: объединение по i и j равно объединению по парам (i,j) в s.sigma.

LaTeX

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

Lean4

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

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