biUnion_finsetSigma — Mathlib

English

For a family of sets f on Sigma α, the union over ij ∈ s.sigma t of f ij equals the union over i ∈ s and j ∈ t i of f ⟨i, j⟩.

Русский

Для семейства множеств f на Σα объединение по ij ∈ s.sigma t равно объединению по i ∈ s и j ∈ t i от f ⟨i, j⟩.

LaTeX

$$$$ \\bigcup_{ij \\in s.sigma t} f(ij) = \\bigcup_{i \\in s} \\bigcup_{j \\in t(i)} f(\\langle i,j\\rangle) $$$$

Lean4

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

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