lt_opow_iff_log_lt' — Mathlib

English

Let b > 1 and c ≠ 0. For any ordinal x, the inequality x < b^c holds exactly when log base b of x is less than c.

Русский

Пусть b > 1 и c ≠ 0. Для любых порядковых чисел x верно: x < b^c тогда log_b x < c, и наоборот.

LaTeX

$$$ 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 `x ≠ 0` rather than `c ≠ 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) (hc : c ≠ 0) : x < b ^ c ↔ log b x < c :=
  lt_iff_lt_of_le_iff_le (opow_le_iff_le_log' hb hc)

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