finTwoArrowEquiv — Mathlib

English

The space of functions Fin(2) → α is equivalent to α × α.

Русский

Множество функций Fin(2) → α эквивалентно α × α.

LaTeX

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

Lean4

/-- The space of functions `Fin 2 → α` is equivalent to `α × α`. See also `piFinTwoEquiv` and
`prodEquivPiFinTwo`. -/
@[simps -fullyApplied]
def finTwoArrowEquiv (α : Type*) : (Fin 2 → α) ≃ α × α :=
  { piFinTwoEquiv fun _ => α with invFun := fun x => ![x.1, x.2] }

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