biUnion_sigma' — Mathlib

English

Let s ⊆ ι, t: ∀ i, Set(α i), and f: ∀ i α i → Set β. Then the iterated union over i ∈ s and j ∈ t i equals the union over ij ∈ s.sigma t of f ij.fst ij.snd.

Русский

Пусть s ⊆ ι, t: ∀ i, Set(α i), и f: ∀ i α i → Set β. Тогда последовательное объединение по i ∈ s и j ∈ t i равно объединению по ij ∈ s.sigma t от f ij.fst ij.snd.

LaTeX

$$$\bigsqcup_{i \in s} \bigsqcup_{j \in t(i)} f(i,j) = \bigsqcup_{(i,j) \in s \sigma t} f(i,j)$$$

Lean4

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

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