le_succ — Mathlib

English

Let α be a preorder with a successor operation. Then every element is below or equal to its successor: for all a, a ≤ succ(a).

Русский

Пусть α — частично упорядоченное множество с переходом к следующему элементу. Тогда любой элемент не выше своего следующего элемента: для любого a выполняется a ≤ succ(a).

LaTeX

$$$\\forall a:\\alpha,\ a \\le \\operatorname{succ}(a)$$$

Lean4

theorem le_succ : ∀ a : α, a ≤ succ a :=
  SuccOrder.le_succ

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