English
There is a natural equivalence between the dependent product over Fin 2 and the ordinary product α0 × α1.
Русский
Существует естественное эквиваленто между зависимым произведением над Fin 2 и обычным произведением α0 × α1.
LaTeX
$$$\\big( \\forall i : \\mathrm{Fin} 2, \\alpha i \\big) \\simeq \\alpha_0 \\times \\alpha_1$$$
Lean4
/-- `Π i : Fin 2, α i` is equivalent to `α 0 × α 1`. See also `finTwoArrowEquiv` for a
non-dependent version and `prodEquivPiFinTwo` for a version with inputs `α β : Type u`. -/
@[simps -fullyApplied]
def piFinTwoEquiv (α : Fin 2 → Type u) : (∀ i, α i) ≃ α 0 × α 1
where
toFun f := (f 0, f 1)
invFun p := Fin.cons p.1 <| Fin.cons p.2 finZeroElim
left_inv _ := funext <| Fin.forall_fin_two.2 ⟨rfl, rfl⟩
