finTwoArrowIso — Mathlib

English

The space of functions Fin 2 → α is order-equivalent to α × α.

Русский

Пространство функций Fin 2 → α упорядоченно эквивалентно α × α.

LaTeX

$$$ (\\mathrm{Fin}\,2 \\to \\alpha) \\simeq_o \\alpha \\times \\alpha $$$

Lean4

/-- The space of functions `Fin 2 → α` is order equivalent to `α × α`. See also
`OrderIso.piFinTwoIso`. -/
def finTwoArrowIso (α : Type*) [Preorder α] : (Fin 2 → α) ≃o α × α :=
  { OrderIso.piFinTwoIso fun _ => α with toEquiv := finTwoArrowEquiv α }

Похожие утверждения