English
Let s be a family of subsets s_i of α indexed by ι, and assume the family is pairwise disjoint. Then the natural map (i, x) with x ∈ s_i into α, given by (i, x) ↦ x, is an embedding.
Русский
Пусть s_i — подпоследовательности α, индексируемые ι, и семейство попарно непересекается. Тогда естественное отображение (i, x) ↦ x из суммарного типа ∑_i s_i в α является вложением (встраиванием).
LaTeX
$$$\text{sigmaSet}(h) : (i, x) \mapsto x \quad\text{является вложением } (i \in ι) \times s_i \hookrightarrow α$$$
Lean4
/-- For an indexed family `s : ι → Set α` of disjoint sets,
the natural injection from the sigma-type `(i : ι) × ↑(s i)` to `α`. -/
@[simps]
def sigmaSet {s : ι → Set α} (h : Pairwise (Disjoint on s)) : (i : ι) × s i ↪ α
where
toFun x := x.2.1
inj' := by
rintro ⟨i, x, hx⟩ ⟨j, -, hx'⟩ rfl
obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)
rfl
