iterate_pred_toZ — Mathlib

English

If i ≥ i0, then iterating pred a number of times equal to (-toZ i0 i).toNat from i0 yields i: pred^[(-toZ i0 i).toNat](i0) = i.

Русский

Если i ≥ i0, то повторяя предшественник(-toZ i0 i).toNat раз, получаем i: pred^[(-toZ i0 i).toNat](i0) = i.

LaTeX

$$$pred^{(-toZ(i_0,i)).toNat}(i_0)=i$$$

Lean4

theorem iterate_pred_toZ (i : ι) (hi : i < i0) : pred^[(-toZ i0 i).toNat] i0 = i :=
  by
  rw [toZ_of_lt hi, neg_neg, Int.toNat_natCast]
  exact Nat.find_spec (exists_pred_iterate_of_le hi.le)

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