English
A successor limit is an element that is not minimal and is a successor prelimit.
Русский
Предел последовательности перехода — это элемент, который не является минимальным и является предпределителем следующего элемента.
LaTeX
$$$IsSuccLimit(a) \equiv (\neg IsMin(a) \land IsSuccPrelimit(a))$$$
Lean4
/-- A successor limit is a value that isn't minimal and doesn't cover any other.
It's so named because in a successor order, a successor limit can't be the successor of anything
smaller.
This previously allowed the element to be minimal. This usage is now covered by `IsSuccPrelimit`. -/
def IsSuccLimit (a : α) : Prop :=
¬IsMin a ∧ IsSuccPrelimit a
