succ_strictMono — Mathlib

English

Assuming NoMaxOrder, the successor map is strictly monotone: x < y implies succ x < succ y.

Русский

При условии NoMaxOrder переход к следующему элементу строго монотонен: x < y ⇒ succ x < succ y.

LaTeX

$$$$ [\mathrm{NoMaxOrder}\;\alpha]\ (x,y):\mathrm{WithBot}\,\alpha,\ x < y \Rightarrow \operatorname{succ} x < \operatorname{succ} y $$$$

Lean4

theorem succ_strictMono [NoMaxOrder α] : StrictMono (succ : WithBot α → α)
  | ⊥, (b : α), hab => by simp
  | (a : α), (b : α), hab => Order.succ_lt_succ (by simpa using hab)

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