pred_eq_pred

Mathlib.Data.Nat.SuccPred

URI: https://scilib.ai/kg/mathlib#Nat.pred_eq_pred

English

Order.succ equals the usual successor function on ℕ.

Русский

Order.succ совпадает с обычной функцией следующего элемента на ℕ.

LaTeX

$$$\\\\operatorname{succ}_{\\mathrm{Order}} = \\operatorname{succ}_{\\\\mathbb N}.$$$

Lean4

@[simp]
theorem pred_eq_pred : Order.pred = pred :=
  rfl

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

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

Разделы

Аффилиация

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