English
IsSuccLimit (a + b) holds iff IsSuccLimit b or (b = 0 and IsSuccLimit a).
Русский
IsSuccLimit(a + b) эквивалентно IsSuccLimit(b) или (b = 0 и IsSuccLimit(a)).
LaTeX
$$$\\text{IsSuccLimit}(a + b) \\\\Leftrightarrow (\\text{IsSuccLimit}(b) \\\\lor (b = 0 \\\\land \\text{IsSuccLimit}(a)))$$$
Lean4
theorem isSuccLimit_add_iff {a b : Ordinal} : IsSuccLimit (a + b) ↔ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a :=
by
constructor <;> intro h
· by_cases h' : b = 0
· rw [h', add_zero] at h
right
exact ⟨h', h⟩
left
rw [← add_sub_cancel a b]
apply isSuccLimit_sub h
suffices a + 0 < a + b by simpa only [add_zero] using this
rwa [add_lt_add_iff_left, Ordinal.pos_iff_ne_zero]
rcases h with (h | ⟨rfl, h⟩)
· exact isSuccLimit_add a h
· simpa only [add_zero]
