succFunEquiv — Mathlib

English

There is a natural equivalence between Fin(n+1) → α and (Fin n → α) × α.

Русский

Существует естественная эквивалентность между Fin(n+1)→α и (Fin n → α) × α.

LaTeX

$$$ (\\mathrm{Fin}(n+1) \\to α) \\cong (\\mathrm{Fin} n \\to α) \\times α$$$

Lean4

/-- `Fin (n + 1) → α` and `(Fin n → α) × α` are equivalent. -/
@[simps!]
def succFunEquiv (α : Type*) (n : ℕ) : (Fin (n + 1) → α) ≃ (Fin n → α) × α :=
  (appendEquiv n 1).symm.trans (Equiv.prodCongrRight fun _ ↦ Equiv.funUnique (Fin 1) α)

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