leftDeriv_mul_log — Mathlib

English

The left derivative of f(x) = x log x at x (x ≠ 0) equals log x + 1.

Русский

Левая производная функции f(x) = x log x в точке x (если x ≠ 0) равна log x + 1.

LaTeX

$$$\text{derivWithin}(x \mapsto x \log x)\, (\mathrm{Iio}\, x) = \log x + 1\quad (x \neq 0)$$$

Lean4

@[simp]
theorem leftDeriv_mul_log {x : ℝ} (hx : x ≠ 0) : derivWithin (fun x ↦ x * log x) (Set.Iio x) x = log x + 1 :=
  (hasDerivAt_mul_log hx).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Iio x)

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