lt_succ — Mathlib

English

If α has no maximum, then every element x of WithBot α is strictly less than its successor: x < x.succ.

Русский

Если у α нет максимального элемента, то каждый x ∈ WithBot α удовлетворяет x < succ(x).

LaTeX

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

Lean4

theorem lt_succ [NoMaxOrder α] (x : WithBot α) : x < x.succ :=
  succ_eq_succ x ▸ Order.lt_succ x

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