toZ_le_iff

Mathlib.Order.SuccPred.LinearLocallyFinite

URI: https://scilib.ai/kg/mathlib#toZ_le_iff

English

For any n, toZ i0 (pred^[n] i0) = -n, provided NoMin order.

Русский

Для любого n, toZ i0 (pred^[n] i0) = -n при условии NoMinOrder.

LaTeX

$$toZ(i_0, Nat.iterate(Order.pred, n, i_0)) = -n$$

Lean4

theorem toZ_le_iff (i j : ι) : toZ i0 i ≤ toZ i0 j ↔ i ≤ j :=
  ⟨le_of_toZ_le, toZ_mono⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru