succ_mono — Mathlib

English

The successor map is monotone: x ≤ y implies succ x ≤ succ y.

Русский

Отображение перехода к следующему элементу монотонно: если x ≤ y, то succ x ≤ succ y.

LaTeX

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

Lean4

theorem succ_mono : Monotone (succ : WithBot α → α)
  | ⊥, _, _ => by simp
  | (a : α), ⊥, hab => by simp at hab
  | (a : α), (b : α), hab => Order.succ_le_succ (by simpa using hab)

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