opow_le_of_le_log — Mathlib

English

If c ≠ 0 and c ≤ log b x then b^c ≤ x.

Русский

Если c ≠ 0 и c ≤ log_b x, то b^c ≤ x.

LaTeX

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

Lean4

theorem opow_le_of_le_log {b x c : Ordinal} (hc : c ≠ 0) (h : c ≤ log b x) : b ^ c ≤ x :=
  by
  obtain hb | hb := le_or_gt b 1
  · rw [log_of_left_le_one hb] at h
    exact (h.not_gt (Ordinal.pos_iff_ne_zero.2 hc)).elim
  · rwa [opow_le_iff_le_log' hb hc]

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