finSuccEquivLast — Mathlib

English

finSuccEquivLast is the specialization finSuccEquiv' applied to the last element, i.e., finSuccEquivLast = finSuccEquiv'(Fin.last n).

Русский

finSuccEquivLast — это частное от finSuccEquiv', полученное при применении к последнему элементу: finSuccEquivLast = finSuccEquiv'(Fin.last n).

LaTeX

$$$$ \\mathrm{finSuccEquivLast} = \\mathrm{finSuccEquiv}'(\\mathrm{Fin.last}(n)). $$$$

Lean4

/-- `Equiv` between `Fin (n + 1)` and `Option (Fin n)` sending `Fin.last n` to `none` -/
def finSuccEquivLast : Fin (n + 1) ≃ Option (Fin n) :=
  finSuccEquiv' (Fin.last n)

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