English
In any ordered structure with a successor operation, provided there is no maximal element and the order is Archimedean, no element is a succ-limit. Equivalently, IsSuccLimit a is false for every a.
Русский
В любой упорядоченной структуре с операцией следующего элемента при отсутствии максимального элемента и викаривающим образом архимедовым свойством, не существует элемента, являющегося пределом поsucc; для каждого a верно, что IsSuccLimit a ложна.
LaTeX
$$$\forall \alpha\, (\text{Preorder } \alpha) \land (\text{SuccOrder } \alpha) \land (\text{IsSuccArchimedean } \alpha) \land (\text{NoMaxOrder } \alpha) \Rightarrow \forall a:\alpha, \neg IsSuccLimit(a)$$$
Lean4
@[simp]
theorem not_isSuccLimit_of_noMax : ¬IsSuccLimit a := fun h ↦ h.not_isMin h.isSuccPrelimit.isMin_of_noMax
