lt_opow_succ_log_self — Mathlib

English

If b > 1 and x ≠ 0, then x < b^{succ(log b x)}.

Русский

Если b > 1 и x ≠ 0, то x < b^{succ(log_b x)}.

LaTeX

$$$\forall \{b,x\in \mathrm{Ordinal}\},\ b > 1 \land x \neq 0 \Rightarrow x < b^{\operatorname{succ}(\log b x)}$$$

Lean4

theorem lt_opow_succ_log_self {b : Ordinal} (hb : 1 < b) (x : Ordinal) : x < b ^ succ (log b x) :=
  by
  rcases eq_or_ne x 0 with (rfl | hx)
  · apply opow_pos _ (zero_lt_one.trans hb)
  · rw [succ_log_def hb hx]
    exact csInf_mem (log_nonempty hb)

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