pred_strictMono — Mathlib

English

Under NoMinOrder, pred is strictly monotone: x < y implies pred x < pred y.

Русский

При условии NoMinOrder предшественник строго монотонен: x < y ⇒ pred x < pred y.

LaTeX

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

Lean4

theorem pred_strictMono [NoMinOrder α] : StrictMono (pred : WithTop α → α)
  | (b : α), ⊤, hab => by simp
  | (a : α), (b : α), hab => Order.pred_lt_pred (by simpa using hab)

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