pred_iterate

Mathlib.Data.Nat.SuccPred

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

← MathLib Explorer

English

The nth iterate of the successor is addition by n: succ^[n](a) = a + n.

Русский

Итерация successor в n шагов даёт a + n: succ^[n](a) = a + n.

LaTeX

$$$\\\\forall a,n \\\\in \\\\mathbb N, \\\\operatorname{succ}^{[n]}(a) = a + n.$$$

Lean4

protected theorem pred_iterate (a : ℕ) : ∀ n, pred^[n] a = a - n
  | 0 => rfl
  | n + 1 => by
    rw [Function.iterate_succ', sub_succ]
    exact congr_arg _ (Nat.pred_iterate a n)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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