orderPred_succ

Mathlib.Data.Fin.SuccPredOrder

URI: https://scilib.ai/kg/mathlib#Fin.orderPred_succ

English

Order.pred(i.succ) = i.castSucc for i ∈ Fin(n).

Русский

Order.pred(i.succ) = i.castSucc для i ∈ Fin(n).

LaTeX

$$$\forall i \in \mathrm{Fin}(n),\ \mathrm{Order.pred}(i.succ) = i.castSucc$$$

Lean4

@[simp]
theorem orderPred_succ {n : ℕ} (i : Fin n) : Order.pred i.succ = i.castSucc :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru