biUnion_sigma — Mathlib

English

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

Русский

Пусть s ⊆ ι, t: ∀ i, Set(α i), и f: Σ i α i → Set β. Тогда объединение по всем ij ∈ s.sigma t f ij равно объединению по 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 biUnion_sigma (s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → Set β) :
    ⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩ :=
  biSup_sigma _ _ _

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