logb_lt_iff_lt_rpow

Mathlib.Analysis.SpecialFunctions.Log.Base

URI: https://scilib.ai/kg/mathlib#Real.logb_lt_iff_lt_rpow

English

If 1 < b and 0 < x, then log_b x < y iff x < b^y.

Русский

Если 1 < b и 0 < x, то log_b x < y эквивалентно x < b^y.

LaTeX

$$$1 < b \land 0 < x \Rightarrow \log_b x < y \iff x < b^{y}.$$$

Lean4

theorem logb_lt_iff_lt_rpow (hx : 0 < x) : logb b x < y ↔ x < b ^ y := by
  rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru