English
A product space α × β is equivalent to the space of functions i : Fin 2 → [α, β] i, i.e., a two-coordinate function.
Русский
Произвольное произведение α × β эквивалентно пространству функций i : Fin 2 → [α, β] i, то есть двухкоординатной функции.
LaTeX
$$$\\alpha \\times \\beta \\cong \\forall i : \\mathrm{Fin}(2), \\![\\alpha, \\beta]\\; i$$$
Lean4
/-- A product space `α × β` is equivalent to the space `Π i : Fin 2, γ i`, where
`γ = Fin.cons α (Fin.cons β finZeroElim)`. See also `piFinTwoEquiv` and
`finTwoArrowEquiv`. -/
@[simps! -fullyApplied]
def prodEquivPiFinTwo (α β : Type u) : α × β ≃ ∀ i : Fin 2, ![α, β] i :=
(piFinTwoEquiv (Fin.cons α (Fin.cons β finZeroElim))).symm
