logb_pos

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

If 1 < b and x > 0, then log_b x > 0 whenever x > 1.

Русский

Если 1 < b и x > 0, то log_b x > 0 при x > 1.

LaTeX

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

Lean4

theorem logb_pos (hx : 1 < x) : 0 < logb b x :=
  by
  rw [logb_pos_iff hb (lt_trans zero_lt_one hx)]
  exact hx

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

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

Разделы

Аффилиация

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