negMulLog_nonneg

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$(0 \le x) \wedge (x \le 1) \Rightarrow 0 \le \operatorname{negMulLog} x$$

Lean4

theorem negMulLog_nonneg {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) : 0 ≤ negMulLog x := by
  simpa only [negMulLog_eq_neg, neg_nonneg] using mul_log_nonpos h1 h2

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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