le_log_of_opow_le — Mathlib

English

If b > 1 and b^c ≤ x, then c ≤ log b x.

Русский

Если b > 1 и b^c ≤ x, тогда c ≤ log_b x.

LaTeX

$$$\forall b,x,c \in \mathrm{Ordinal},\ b > 1 \land b^{c} \le x \Rightarrow c \le \log b x$$$

Lean4

theorem le_log_of_opow_le {b x c : Ordinal} (hb : 1 < b) (h : b ^ c ≤ x) : c ≤ log b x :=
  by
  obtain rfl | hx := eq_or_ne x 0
  · rw [Ordinal.le_zero, opow_eq_zero] at h
    exact (zero_lt_one.asymm <| h.1 ▸ hb).elim
  · exact (opow_le_iff_le_log hb hx).1 h

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