lt_succ

Mathlib.Order.SuccPred.Basic

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

English

In a no-maximum order, every element is strictly less than its successor.

Русский

В порядка без максимума каждый элемент строго меньше своего successor.

LaTeX

$$$a < \\operatorname{succ}(a)$$$

Lean4

theorem lt_succ (a : α) : a < succ a :=
  lt_succ_of_not_isMax <| not_isMax a

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

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

Разделы

Аффилиация

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