English
The type of dependent functions on a sum type ι ⊕ ι' is equivalent to the product of the dependent function spaces on ι and on ι'.
Русский
Тип зависимых функций на суммном типе ι ⊕ ι' эквивалентен произведению пространств зависимых функций на ι и на ι'.
LaTeX
$$$\{ι, ι' : Type\} \to (π : ι \oplus ι' \to Type*)\;\;:\; (∀ i, π i) \cong (∀ i, π (Sum.inl i)) \times ∀ i', π (Sum.inr i')$$$
Lean4
/-- The type of dependent functions on a sum type `ι ⊕ ι'` is equivalent to the type of pairs of
functions on `ι` and on `ι'`. This is a dependent version of `Equiv.sumArrowEquivProdArrow`. -/
@[simps]
def sumPiEquivProdPi {ι ι'} (π : ι ⊕ ι' → Type*) : (∀ i, π i) ≃ (∀ i, π (inl i)) × ∀ i', π (inr i')
where
toFun f := ⟨fun i => f (inl i), fun i' => f (inr i')⟩
invFun g := Sum.rec g.1 g.2
left_inv f := by ext (i | i) <;> rfl
