lt_succ_iff_ne_top

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.lt_succ_iff_ne_top

English

a < succ a if and only if a is not the top element.

Русский

a < succ a тогда и только тогда, когда a не является верхом.

LaTeX

$$a < succ a \iff a \neq \\top$$

Lean4

theorem lt_succ_iff_ne_top : a < succ a ↔ a ≠ ⊤ :=
  lt_succ_iff_not_isMax.trans not_isMax_iff_ne_top

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

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

Разделы

Аффилиация

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