English
If c > 0, a < ω^c and b < ω, then a * b < ω^c.
Русский
Если c > 0, a < ω^c и b < ω, то a * b < ω^c.
LaTeX
$$$(0 < c) \land (a < \omega^c) \land (b < \omega) \Rightarrow a * b < \omega^c.$$$
Lean4
theorem mul_lt_omega0_opow (c0 : 0 < c) (ha : a < ω ^ c) (hb : b < ω) : a * b < ω ^ c :=
by
rcases zero_or_succ_or_isSuccLimit c with (rfl | ⟨c, rfl⟩ | l)
· exact (lt_irrefl _).elim c0
· rw [opow_succ] at ha
obtain ⟨n, hn, an⟩ := ((isNormal_mul_right <| opow_pos _ omega0_pos).limit_lt isSuccLimit_omega0).1 ha
apply (mul_le_mul_right' (le_of_lt an) _).trans_lt
rw [opow_succ, mul_assoc]
gcongr
exacts [opow_pos _ omega0_pos, principal_mul_omega0 hn hb]
· rcases ((isNormal_opow one_lt_omega0).limit_lt l).1 ha with ⟨x, hx, ax⟩
refine (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_
rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega0]
exact l.succ_lt hx
