English
If a < ω^b, then a + ω^b = ω^b.
Русский
Если a < ω^b, то a + ω^b = ω^b.
LaTeX
$$$a < \omega^b \Rightarrow a + \omega^b = \omega^b.$$$
Lean4
theorem add_omega0_opow (h : a < ω ^ b) : a + ω ^ b = ω ^ b :=
by
refine le_antisymm ?_ (le_add_left _ a)
induction b using limitRecOn with
| zero =>
rw [opow_zero, ← succ_zero, lt_succ_iff, Ordinal.le_zero] at h
rw [h, zero_add]
| succ =>
rw [opow_succ] at h
rcases (lt_mul_iff_of_isSuccLimit isSuccLimit_omega0).1 h with ⟨x, xo, ax⟩
apply (add_le_add_right ax.le _).trans
rw [opow_succ, ← mul_add, add_omega0 xo]
| limit b l IH =>
rcases (lt_opow_of_isSuccLimit omega0_ne_zero l).1 h with ⟨x, xb, ax⟩
apply (((isNormal_add_right a).trans <| isNormal_opow one_lt_omega0).limit_le l).2
intro y yb
calc
a + ω ^ y ≤ a + ω ^ max x y := add_le_add_left (opow_le_opow_right omega0_pos (le_max_right x y)) _
_ ≤ ω ^ max x y := (IH _ (max_lt xb yb) <| ax.trans_le <| opow_le_opow_right omega0_pos <| le_max_left x y)
_ ≤ ω ^ b := opow_le_opow_right omega0_pos <| (max_lt xb yb).le
