English
A type indexed by a disjoint sum is equivalent to the sum of the indexed types: (Σ i, t i) ≃ (Σ i, t (Sum.inl i)) ⊕ (Σ i, t (Sum.inr i)).
Русский
Тип, индексируемый по расщепляющимся суммам, эквивалентен сумме индексированных типов: (Σ i, t i) ≃ (Σ i, t (Sum.inl i)) ⊕ (Σ i, t (Sum.inr i)).
LaTeX
$$$$\\Sigma i:\\mathrm{Sum} \\alpha \\beta\\, t\,i \\cong (\\Sigma i:\\alpha, t(\\mathrm{Sum.inl } i)) \\oplus (\\Sigma i:\\beta, t(\\mathrm{Sum.inr } i)).$$$$
Lean4
/-- A type indexed by disjoint sums of types is equivalent to the sum of the sums. Compare with
`Equiv.sigmaSumDistrib` which has the sums as the output type. -/
@[simps]
def sumSigmaDistrib {α β} (t : α ⊕ β → Type*) : (Σ i, t i) ≃ (Σ i, t (.inl i)) ⊕ (Σ i, t (.inr i)) :=
⟨(match · with
| .mk (.inl x) y => .inl ⟨x, y⟩
| .mk (.inr x) y => .inr ⟨x, y⟩),
Sum.elim (fun a ↦ ⟨.inl a.1, a.2⟩) (fun b ↦ ⟨.inr b.1, b.2⟩), by rintro ⟨x | x, y⟩ <;> simp, by
rintro (⟨x, y⟩ | ⟨x, y⟩) <;> simp⟩
