lt_omega0_opow_succ — Mathlib

English

For any b, a < ω^{succ b} iff there exists n ∈ N with a < ω^b · n.

Русский

Для любого b: a < ω^{succ b} тогда и только тогда существует n ∈ N, такое что a < ω^b · n.

LaTeX

$$$ a < \omega^{\operatorname{succ} b} \iff \exists n \in \mathbb{N}, a < \omega^b \cdot n $$$

Lean4

theorem lt_omega0_opow_succ {a b : Ordinal} : a < ω ^ succ b ↔ ∃ n : ℕ, a < ω ^ b * n :=
  by
  refine ⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt (lt_succ b) n)⟩
  obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (succ_ne_zero b)).1 ha
  refine ⟨n, hn.trans_le (mul_le_mul_right' ?_ _)⟩
  rwa [opow_le_opow_iff_right one_lt_omega0, ← lt_succ_iff]

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