biUnion_finsetSigma' — Mathlib

English

A Set-valued version of the Sigma-BiUnion equality with a prime variant; union over sigma t equals nested unions.

Русский

Версия для множеств с апострофом, равенство объединений над сигмой превращается в вложенные объединения.

LaTeX

$$$$ \bigcup_{ij \in s.sigma t} f_{ij} = \bigcup_{i \in s} \bigcup_{j \in t_i} f_{ij} $$$$

Lean4

theorem _root_.Set.biUnion_finsetSigma' (s : Finset ι) (t : ∀ i, Finset (α i)) (f : ∀ i, α i → Set β) :
    ⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ s.sigma t, f ij.fst ij.snd :=
  biSup_finsetSigma' _ _ _

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