add_one_le_iff

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.add_one_le_iff

English

ToNat n equals n iff n ≠ ⊤.

Русский

ToNat n равен n тогда и только тогда, когда n ≠ ⊤.

LaTeX

$$$\\\\operatorname{toNat}(n) = n \\\\iff n \\\\neq \\\\top$$$

Lean4

theorem add_one_le_iff (hm : m ≠ ⊤) : m + 1 ≤ n ↔ m < n :=
  Order.add_one_le_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)

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

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

Разделы

Аффилиация

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