lt_opow_iff_log_lt — Mathlib

English

For b > 1 and x ≠ 0, x < b^c iff log b x < c.

Русский

Для b > 1 и x ≠ 0, x < b^c тогда и только тогда, когда log_b x < c.

LaTeX

$$$\forall b,x,c \in \mathrm{Ordinal},\ b > 1 \land x \neq 0 \Rightarrow x < b^{c} \iff \log b x < c$$$

Lean4

/-- `opow b` and `log b` (almost) form a Galois connection.

See `lt_opow_iff_log_lt'` for a variant assuming `c ≠ 0` rather than `x ≠ 0`. See also
`lt_opow_of_log_lt` and `lt_log_of_lt_opow`, which are both separate implications under weaker
assumptions. -/
theorem lt_opow_iff_log_lt {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : x < b ^ c ↔ log b x < c :=
  lt_iff_lt_of_le_iff_le (opow_le_iff_le_log hb hx)

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