lt_succ_of_le_of_not_isMax

Mathlib.Order.SuccPred.Basic

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

English

If b ≤ a and a is not maximal, then b < succ(a).

Русский

Если b ≤ a и a не максимален, тогда b < succ(a).

LaTeX

$$$(b \\le a) \\land \\neg \\mathrm{IsMax}(a) \\Rightarrow b < \\operatorname{succ}(a)$$$

Lean4

theorem lt_succ_of_le_of_not_isMax (hab : b ≤ a) (ha : ¬IsMax a) : b < succ a :=
  hab.trans_lt <| lt_succ_of_not_isMax ha

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

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

Разделы

Аффилиация

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