toZ_of_ge — Mathlib

English

If i0 ≤ i, then toZ i0 i equals the unique integer N found by the successor-iteration bound.

Русский

Если i0 ≤ i, то toZ i0 i равен уникальному целому N, найденному по границе поитерации successor.

LaTeX

$$$i_0 \\le i \\Rightarrow \\mathrm{toZ}(i_0,i) = \\mathrm{Nat.find}(\\exists\\succ\\text{_iterate_of_le}(i,i_0))$$$

Lean4

theorem toZ_of_ge (hi : i0 ≤ i) : toZ i0 i = Nat.find (exists_succ_iterate_of_le hi) :=
  dif_pos hi

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