lt_omega0_opow — Mathlib

English

If a < ω^b, then there exists c < b and n ∈ N with a < ω^c · n.

Русский

Если a < ω^b, то существует c < b и n ∈ N such that a < ω^c · n.

LaTeX

$$$ a < \omega^b \Rightarrow \exists c < b, \exists n \in \mathbb{N}, a < \omega^c \cdot n $$$

Lean4

theorem lt_omega0_opow {a b : Ordinal} (hb : b ≠ 0) : a < ω ^ b ↔ ∃ c < b, ∃ n : ℕ, a < ω ^ c * n :=
  by
  refine ⟨fun ha ↦ ⟨_, lt_log_of_lt_opow hb ha, ?_⟩, fun ⟨c, hc, n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt hc n)⟩
  obtain ⟨n, hn⟩ := lt_omega0.1 (div_opow_log_lt a one_lt_omega0)
  use n.succ
  rw [natCast_succ, ← hn]
  exact lt_mul_succ_div a (opow_ne_zero _ omega0_ne_zero)

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