English
Let α be a canonically ordered additive monoid with one, equipped with a SuccAddOrder and a bottom element. Then for every natural number n, the element n embedded into α is not a succ-limit point; i.e., IsSuccLimit(n : α) is false.
Русский
Пусть α — канонически упорядоченный аддитивный моноид с единицей, имеющий SuccAddOrder и нулевой элемент. Тогда для каждого натурального числа n элемент n, воспринятый как элемент α, не является предельной точкойsucc; то есть IsSuccLimit(n : α) ложно.
LaTeX
$$$\forall n \in \mathbb{N},\ \neg \mathrm{IsSuccLimit}(n:\alpha)$$$
Lean4
theorem not_isSuccLimit_natCast [AddMonoidWithOne α] [SuccAddOrder α] [OrderBot α] [CanonicallyOrderedAdd α] (n : ℕ) :
¬IsSuccLimit (n : α) := fun h ↦ (h.natCast_lt n).false
