toZ_of_lt — Mathlib

English

If i < i0, then toZ i0 i equals the negatedNat find of the predecessor-iteration bound.

Русский

Если i < i0, то toZ i0 i равно отрицательному finding-у границы предшественников.

LaTeX

$$$i < i_0 \\Rightarrow \\mathrm{toZ}(i_0,i) = -\\mathrm{Nat.find}(\\exists\\text{pred\\_iterate\_of\_le}(i,i_0.\\text{le}))$$$

Lean4

theorem toZ_of_lt (hi : i < i0) : toZ i0 i = -Nat.find (exists_pred_iterate_of_le (α := ι) hi.le) :=
  dif_neg (not_le.mpr hi)

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