logb_pos_iff

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

For 1 < b and 0 < x, log_b x > 0 if and only if x > 1.

Русский

Для 1 < b и 0 < x верно: log_b x > 0 тогда x > 1.

LaTeX

$$$1 < b \land 0 < x \Rightarrow 0 < \log_b x \iff x > 1.$$$

Lean4

theorem logb_pos_iff (hx : 0 < x) : 0 < logb b x ↔ 1 < x :=
  by
  rw [← @logb_one b]
  rw [logb_lt_logb_iff hb zero_lt_one hx]

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

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

Разделы

Аффилиация

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