succ_iterate — Mathlib

English

Iterating the successor n times yields addition by n: succ^{[n]}(x) = x + n.

Русский

Повторное применение successor n раз эквивалентно сложению на n: succ^{[n]}(x) = x + n.

LaTeX

$$$\\\\mathrm{succ}^{[n]}(x) = x + n.$$$

Lean4

@[simp]
theorem succ_iterate [AddMonoidWithOne α] [SuccAddOrder α] (x : α) (n : ℕ) : succ^[n] x = x + n := by
  induction n with
  | zero => rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
  | succ n IH => rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

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