negMulLog_one

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

English

The function f(x) = -x log x satisfies f(1) = 0.

Русский

Функция f(x) = -x log x принимает значение 0 при x = 1.

LaTeX

$$$\operatorname{negMulLog}(1) = 0$$$

Lean4

@[simp]
theorem negMulLog_one : negMulLog (1 : ℝ) = 0 := by simp [negMulLog]

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

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

Разделы

Аффилиация

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