logb_nonpos

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

For 1 < b and 0 ≤ x ≤ 1, log_b x ≤ 0.

Русский

Для 1 < b и 0 ≤ x ≤ 1: log_b x ≤ 0.

LaTeX

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

Lean4

theorem logb_nonpos (hx : 0 ≤ x) (h'x : x ≤ 1) : logb b x ≤ 0 :=
  (logb_nonpos_iff' hb hx).2 h'x

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

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

Разделы

Аффилиация

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