pred_le_pred

Mathlib.Order.SuccPred.WithBot

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

English

If x ≤ y, then x.pred ≤ y.pred.

Русский

Если x ≤ y, тогда x.pred ≤ y.pred.

LaTeX

$$$$ \forall x,y:\mathrm{WithTop}\,\alpha,\ x \le y \Rightarrow x.{\text{pred}} \le y.{\text{pred}} $$$$

Lean4

@[gcongr]
theorem pred_le_pred (hxy : x ≤ y) : x.pred ≤ y.pred :=
  pred_mono hxy

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

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

Разделы

Аффилиация

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