mul_log_nonpos

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

English

If 0 ≤ x ≤ 1, then x log x ≤ 0.

Русский

Если 0 ≤ x ≤ 1, то x log x ≤ 0.

LaTeX

$$$0 \le x \le 1 \Rightarrow x \log x \le 0$$$

Lean4

theorem mul_log_nonpos {x : ℝ} (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x * log x ≤ 0 :=
  mul_nonpos_of_nonneg_of_nonpos hx₀ (log_nonpos hx₀ hx₁)

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

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

Разделы

Аффилиация

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