toZ_nonneg

Mathlib.Order.SuccPred.LinearLocallyFinite

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

English

If i0 ≤ i, then the integer toZ i0 i is nonnegative: 0 ≤ toZ i0 i.

Русский

Если i0 ≤ i, то toZ i0 i неотрицательно: 0 ≤ toZ i0 i.

LaTeX

$$0 \le toZ(i_0,i)$$

Lean4

theorem toZ_nonneg (hi : i0 ≤ i) : 0 ≤ toZ i0 i := by rw [toZ_of_ge hi]; exact Int.natCast_nonneg _

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

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

Разделы

Аффилиация

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