below_of_lt' — Mathlib

English

For any o and b, if repr o < ω^b and NF o, then NFBelow o b.

Русский

Для любого o и b, если repr o < ω^b и NF o, то NFBelow o b.

LaTeX

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

Lean4

theorem below_of_lt' : ∀ {o b}, repr o < ω ^ b → NF o → NFBelow o b
  | 0, _, _, _ => NFBelow.zero
  | ONote.oadd _ _ _, _, H, h =>
    h.below_of_lt <| (opow_lt_opow_iff_right one_lt_omega0).1 <| lt_of_le_of_lt (omega0_le_oadd _ _ _) H

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