English
Let (s_i) be a family of subsets of β such that every element b ∈ β belongs to exactly one s_i. Then there is a bijection between the disjoint sum Σ i, s_i and β, given by the natural projection to β and its inverse sending b to the unique pair witnessing b ∈ s_i.
Русский
Пусть family s_i ⊆ β разбивает β на непересекающиеся части: каждый b ∈ β принадлежит ровно одной s_i. Тогда существует биекция между разобщённой суммой Σ i, s_i и β, заданная естественным отображением в β и обратной отправкой b в уникальную пару (i, b) с b ∈ s_i.
LaTeX
$$$(\\forall b : β,\\ ∃! i, b ∈ s_i) \\Rightarrow (Σ i, s_i) \\cong β$$$
Lean4
/-- Equivalence from the disjoint union of a family of sets forming a partition of `β`, to `β`
itself. -/
noncomputable def sigmaEquiv (s : α → Set β) (hs : ∀ b, ∃! i, b ∈ s i) : (Σ i, s i) ≃ β
where
toFun
| ⟨_, b⟩ => b
invFun b := ⟨(hs b).choose, b, (hs b).choose_spec.1⟩
left_inv
| ⟨i, b, hb⟩ => Sigma.subtype_ext ((hs b).choose_spec.2 i hb).symm rfl
