unionEqSigmaOfDisjoint — Mathlib

English

Let t be a family of subsets t_i that is pairwise disjoint. Then the union ⋃ i, t_i is naturally bijective to the dependent sum Σ i, t_i.

Русский

Пусть t = (t_i) — параллельно разобщённая совокупность подмножеств. Тогда объединение ⋃ i t_i и зависимая сумма Σ i, t_i образуют биективное соответствие.

LaTeX

$$$(⋃ i, t i) \\cong Σ i, t i$$$

Lean4

/-- Equivalence between a disjoint union and a dependent sum. -/
noncomputable def unionEqSigmaOfDisjoint {t : α → Set β} (h : Pairwise (Disjoint on t)) : (⋃ i, t i) ≃ Σ i, t i :=
  (Equiv.ofBijective _ <| sigmaToiUnion_bijective t h).symm

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