English
An indexed sum of disjoint sums is equivalent to the sum of the indexed sums: (Σ i, α i ⊕ β i) ≃ (Σ i, α i) ⊕ (Σ i, β i).
Русский
Индексированная сумма по непересекающимся суммам равна сумме индексированных сумм: (Σ i, α i ⊕ β i) ≃ (Σ i, α i) ⊕ (Σ i, β i).
LaTeX
$$$$\\Sigma i:\\iota\\, (\\alpha(i) \\oplus \\beta(i)) \\cong (\\Sigma i:\\iota\\, \\alpha(i)) \\oplus (\\Sigma i:\\iota\\, \\beta(i)).$$$$
Lean4
/-- An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. Compare
with `Equiv.sumSigmaDistrib` which is indexed by sums. -/
@[simps]
def sigmaSumDistrib {ι} (α β : ι → Type*) : (Σ i, α i ⊕ β i) ≃ (Σ i, α i) ⊕ (Σ i, β i) :=
⟨fun p => p.2.map (Sigma.mk p.1) (Sigma.mk p.1),
Sum.elim (Sigma.map id fun _ => Sum.inl) (Sigma.map id fun _ => Sum.inr), fun p => by
rcases p with ⟨i, a | b⟩ <;> rfl, fun p => by rcases p with (⟨i, a⟩ | ⟨i, b⟩) <;> rfl⟩
