succ_iterate

Mathlib.Data.Nat.SuccPred

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

English

Order.pred equals the usual predecessor function on ℕ.

Русский

Order.pred совпадает с обычной функцией предшественника на ℕ.

LaTeX

$$$\\\\operatorname{pred}_{\\\\mathrm{Order}} = \\operatorname{pred}.$$$

Lean4

protected theorem succ_iterate (a : ℕ) : ∀ n, succ^[n] a = a + n :=
  Order.succ_iterate a

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

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

Разделы

Аффилиация

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