English
For any o and any f with domain below o, and any i with i < o, f(i,i<o) < blsub(o,f).
Русский
Для любого o и любой функции f, определенной ниже o, и любого i с i < o, выполняется f(i, i<o) < blsub(o,f).
LaTeX
$$$\forall o : \mathrm{Ordinal},\ \forall f : \forall a < o, \mathrm{Ordinal},\forall i\,\forall h,\ f(i,h) < \mathrm{blsub}(o,f)$$$
Lean4
theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b :=
by
nth_rw 1 [← opow_one a]
rcases le_or_gt a 1 with a1 | a1
· rcases lt_or_eq_of_le a1 with a0 | a1
· rw [lt_one_iff_zero] at a0
rw [a0, zero_opow Ordinal.one_ne_zero]
exact Ordinal.zero_le _
rw [a1, one_opow, one_opow]
rwa [opow_le_opow_iff_right a1, one_le_iff_pos]
