succ_lt_succ

Mathlib.Order.SuccPred.WithBot

URI: https://scilib.ai/kg/mathlib#WithBot.succ_lt_succ

English

If x < y, then x.succ < y.succ (noMaxOrder assumption is used similarly).

Русский

Если x < y, то x.succ < y.succ.

LaTeX

$$$$ \forall x,y:\mathrm{WithBot}\,\alpha,\ x < y \Rightarrow \operatorname{succ} x < \operatorname{succ} y $$$$

Lean4

@[gcongr]
theorem succ_lt_succ [NoMaxOrder α] (hxy : x < y) : x.succ < y.succ :=
  succ_strictMono hxy

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

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

Разделы

Аффилиация

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