opow_log_le_self — Mathlib

English

For any base b and x with x ≠ 0, b^{log b x} ≤ x.

Русский

Для любого основания b и x с x ≠ 0, b^{log_b x} ≤ x.

LaTeX

$$$\forall b,x \in \mathrm{Ordinal},\ x \neq 0 \Rightarrow b^{\log b x} \le x$$$

Lean4

theorem opow_log_le_self (b : Ordinal) {x : Ordinal} (hx : x ≠ 0) : b ^ log b x ≤ x :=
  by
  rcases eq_or_ne b 0 with (rfl | b0)
  · exact (zero_opow_le _).trans (one_le_iff_ne_zero.2 hx)
  rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with (hb | rfl)
  · refine le_of_not_gt fun h => (lt_succ (log b x)).not_ge ?_
    have := @csInf_le' _ _ {o | x < b ^ o} _ h
    rwa [← succ_log_def hb hx] at this
  · rwa [one_opow, one_le_iff_ne_zero]

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