pred_mono — Mathlib

English

The predecessor map pred is monotone: x ≤ y implies pred x ≤ pred y.

Русский

Отображение предшественника предмонотонно: x ≤ y ⇒ pred x ≤ pred y.

LaTeX

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

Lean4

theorem pred_mono : Monotone (pred : WithTop α → α)
  | _, ⊤, _ => by simp
  | ⊤, (a : α), hab => by simp at hab
  | (a : α), (b : α), hab => Order.pred_le_pred (by simpa using hab)

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