English
The equivalence between a product of dependent function types and a single dependent function type on a sum: ((∀ i, π i) × ∀ i', π' i') ≃ ∀ i, Sum.elim π π' i.
Русский
Эквивалентность между произведением зависимых функций и одной зависимой функции на сумме: ((∀ i, π i) × ∀ i', π' i') ≃ ∀ i, Sum.elim π i π' i.
LaTeX
$$$\left( (\forall i, \pi i) \times (\forall i', \pi' i') \right) \cong \forall i, Sum.elim \pi \pi' i$$$
Lean4
/-- The equivalence between a product of two dependent functions types and a single dependent
function type. Basically a symmetric version of `Equiv.sumPiEquivProdPi`. -/
@[simps!]
def prodPiEquivSumPi {ι ι'} (π : ι → Type u) (π' : ι' → Type u) : ((∀ i, π i) × ∀ i', π' i') ≃ ∀ i, Sum.elim π π' i :=
sumPiEquivProdPi (Sum.elim π π') |>.symm
