iterate_succ_toZ — Mathlib

English

For any i with i0 ≤ i, applying succ repeatedly a number of times equal to the natural value of toZ i0 i reaches i: succ^{[(toZ i0 i).toNat]}(i0) = i.

Русский

Пусть i0 ≤ i. Применение successor последовательно столько раз, сколько равно toNat(toZ i0 i), приводит к i: succ^{[(toZ i0 i).toNat]}(i0) = i.

LaTeX

$$$succ^{[(toZ(i_0,i)).toNat]}(i_0)=i$$$

Lean4

theorem iterate_succ_toZ (i : ι) (hi : i0 ≤ i) : succ^[(toZ i0 i).toNat] i0 = i :=
  by
  rw [toZ_of_ge hi, Int.toNat_natCast]
  exact Nat.find_spec (exists_succ_iterate_of_le hi)

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