English
The successor operator on a SuccOrder: if a is not maximal, succ a is the least element greater than a; if a is maximal, succ a = a.
Русский
Оператор successor на SuccOrder: если a не максимален, то succ a — наименьший элемент, больший a; если a максимален, то succ a = a.
LaTeX
$$$\\text{succ}(a) = \\begin{cases} \\text{минимальный } b > a, & \\text{если } a \\text{ не максимален}, \\\\ a, & \\text{если } a \\text{ максимален}. \\end{cases}$$$
Lean4
/-- The successor of an element. If `a` is not maximal, then `succ a` is the least element greater
than `a`. If `a` is maximal, then `succ a = a`. -/
def succ : α → α :=
SuccOrder.succ
