not_continuousAt_deriv_mul_log_zero

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

← MathLib Explorer

English

The derivative of x log x is not continuous at 0.

Русский

Производная функции x log x не непрерывна в точке 0.

LaTeX

$$$\neg \text{ContinuousAt}\left( x \mapsto \frac{d}{dx}\bigl(x \log x\bigr) \right)\Big|_{x=0}$$$

Lean4

theorem not_continuousAt_deriv_mul_log_zero : ¬ContinuousAt (deriv (fun (x : ℝ) ↦ x * log x)) 0 :=
  not_continuousAt_of_tendsto tendsto_deriv_mul_log_nhdsWithin_zero nhdsWithin_le_nhds (by simp)

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

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

Разделы

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

Аффилиация

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