rightDeriv_mul_log — Mathlib

English

The right 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{Ioi}\, x) = \log x + 1\quad (x \neq 0)$$$

Lean4

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

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