opow_le_iff_le_log' — Mathlib

English

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

Русский

Если b > 1 и c ≠ 0, тогда b^c ≤ x эквивалентно c ≤ log_b x.

LaTeX

$$$\forall b,x,c \in \mathrm{Ordinal},\ b > 1 \Rightarrow c \neq 0 \Rightarrow (b^{c} \le x \iff 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 `x ≠ 0` rather than `c ≠ 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) (hc : c ≠ 0) : b ^ c ≤ x ↔ c ≤ log b x :=
  by
  obtain rfl | hx := eq_or_ne x 0
  · simp [hc, (zero_lt_one.trans hb).ne']
  · exact opow_le_iff_le_log hb hx

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