English
If the order has a bottom element, then IsSuccLimit a holds exactly when a is not the bottom and a is a succ-prelimit.
Русский
Если в порядке есть нулевой элемент, то IsSuccLimit a выполняется тогда и только тогда, когда a не равен нижнему пределу и a является succ-предпределом.
LaTeX
$$$\forall \alpha\, (\text{PartialOrder } \alpha) \land (\text{OrderBot } \alpha) \Rightarrow IsSuccLimit(a) \leftrightarrow (a \neq \bot) \land IsSuccPrelimit(a)$$$
Lean4
theorem isSuccLimit_iff [OrderBot α] : IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a := by rw [IsSuccLimit, isMin_iff_eq_bot]