orderSucc_eq — Mathlib

English

The order successor on Fin is given by the last-cases construction: Order.succ = Fin.lastCases (Fin.last n) Fin.succ.

Русский

Порядок перехода в Fin задаётся конструктором последнего элемента: Order.succ = Fin.lastCases (Fin.last n) Fin.succ.

LaTeX

$$$\mathrm{Order.succ} = \mathrm{Fin.lastCases}(\mathrm{Fin.last}\, n)\, \mathrm{Fin.succ}$$$

Lean4

theorem orderSucc_eq {n : ℕ} : Order.succ = Fin.lastCases (Fin.last n) Fin.succ :=
  rfl

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