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
/-- `opow b` and `log b` (almost) form a Galois connection.
See `opow_le_iff_le_log'` for a variant assuming `c ≠ 0` rather than `x ≠ 0`. See also
`le_log_of_opow_le` and `opow_le_of_le_log`, which are both separate implications under weaker
assumptions. -/
theorem opow_le_iff_le_log {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : b ^ c ≤ x ↔ c ≤ log b x :=
by
constructor <;> intro h
· apply le_of_not_gt
intro hn
apply (lt_opow_succ_log_self hb x).not_ge <| ((opow_le_opow_iff_right hb).2 <| succ_le_of_lt hn).trans h
· exact ((opow_le_opow_iff_right hb).2 h).trans <| opow_log_le_self b hx
