English
For any ordinal a, IsSuccLimit a iff a ≠ 0 and ω divides a.
Русский
Для любого ординала a верно: a является пределом-непосредствующим тогда и только если a ≠ 0 и ω делит a.
LaTeX
$$$\forall a:\mathrm{Ordinal},\ \mathrm{IsSuccLimit}(a) \iff a \neq 0 \wedge \omega \mid a$$$
Lean4
theorem isSuccLimit_iff_omega0_dvd {a : Ordinal} : IsSuccLimit a ↔ a ≠ 0 ∧ ω ∣ a :=
by
refine ⟨fun l => ⟨l.ne_bot, ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩⟩, fun h => ?_⟩
· refine l.le_iff_forall_le.2 fun x hx => le_of_lt ?_
rw [← div_lt omega0_ne_zero, ← succ_le_iff, le_div omega0_ne_zero, mul_succ,
add_le_iff_of_isSuccLimit isSuccLimit_omega0]
intro b hb
rcases lt_omega0.1 hb with ⟨n, rfl⟩
exact
(add_le_add_right (mul_div_le _ _) _).trans (lt_sub.1 <| natCast_lt_of_isSuccLimit (isSuccLimit_sub l hx) _).le
· rcases h with ⟨a0, b, rfl⟩
refine isSuccLimit_mul_left isSuccLimit_omega0 (Ordinal.pos_iff_ne_zero.2 <| mt ?_ a0)
intro e
simp only [e, mul_zero]
