repr_lt — Mathlib

English

If NFBelow o b, then repr(o) < ω^b.

Русский

Если o ниже b в NFBelow, то repr(o) < ω^b.

LaTeX

$$$NFBelow(o,b) \Rightarrow \operatorname{repr}(o) < \omega^{b}$$$

Lean4

theorem repr_lt {o b} (h : NFBelow o b) : repr o < ω ^ b := by
  induction h with
  | zero => exact opow_pos _ omega0_pos
  | oadd' _ _ h₃ _ IH =>
    rw [repr]
    apply ((add_lt_add_iff_left _).2 IH).trans_le
    rw [← mul_succ]
    apply (mul_le_mul_left' (succ_le_of_lt (nat_lt_omega0 _)) _).trans
    rw [← opow_succ]
    exact opow_le_opow_right omega0_pos (succ_le_of_lt h₃)

Похожие утверждения