English
The family of functions from Fin 2 to α is order-isomorphic to the product α0 × α1; i.e., the two-element index family is order-equivalent to a pair of elements.
Русский
Множество функций из Fin 2 в α упорядоченно изоморфно произведению α0 × α1; т.е. двумерная семантика индексов эквивалентна паре элементов.
LaTeX
$$$ (\forall i:\mathrm{Fin}2,\; \alpha i) \simeq_o (\alpha 0 \times \alpha 1) $$$
Lean4
/-- `Π i : Fin 2, α i` is order equivalent to `α 0 × α 1`. See also `OrderIso.finTwoArrowEquiv`
for a non-dependent version. -/
def piFinTwoIso (α : Fin 2 → Type*) [∀ i, Preorder (α i)] : (∀ i, α i) ≃o α 0 × α 1
where
toEquiv := piFinTwoEquiv α
map_rel_iff' := Iff.symm Fin.forall_fin_two
