succ_le_succ

Mathlib.Order.SuccPred.WithBot

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

English

If x ≤ y, then x.succ ≤ y.succ.

Русский

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

LaTeX

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

Lean4

@[gcongr]
theorem succ_le_succ (hxy : x ≤ y) : x.succ ≤ y.succ :=
  succ_mono hxy

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

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

Разделы

Аффилиация

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