pred_lt_pred

Mathlib.Order.SuccPred.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.pred_lt_pred

English

Under NoMinOrder, x < y implies x.pred < y.pred.

Русский

При NoMinOrder: x < y ⇒ x.pred < y.pred.

LaTeX

$$$$ [\mathrm{NoMinOrder}\;\alpha]\ (x,y):\mathrm{WithTop}\,\alpha,\ x < y \Rightarrow x.pred < y.pred $$$$

Lean4

@[gcongr]
theorem pred_lt_pred [NoMinOrder α] (hxy : x < y) : x.pred < y.pred :=
  pred_strictMono hxy

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

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

Разделы

Аффилиация

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