English
The dependent-sum version of the previous statement: the type of dependent functions on a sum is equivalent to the product of dependent function spaces.
Русский
Зависимая сумма: тип зависимых функций на сумме эквивалентен произведению зависимых функций на части суммы.
LaTeX
$$$\text{sumPiEquivProdPi} : (ι \oplus ι') \to Type* \;\; :\; (∀ i, π i) \cong (∀ i, π (Sum.inl i)) \times ∀ i', π (Sum.inr i')$$$
Lean4
/-- The type of functions on a sum type `α ⊕ β` is equivalent to the type of pairs of functions
on `α` and on `β`. -/
def sumArrowEquivProdArrow (α β γ : Type*) : (α ⊕ β → γ) ≃ (α → γ) × (β → γ) :=
⟨fun f => (f ∘ inl, f ∘ inr), fun p => Sum.elim p.1 p.2, fun f => by ext ⟨⟩ <;> rfl, fun p =>
by
cases p
rfl⟩
