hasDerivAt_mul_log — Mathlib

English

For x ≠ 0, HasDerivAt (λx, x log x) at x with value log x + 1.

Русский

Для x ≠ 0 имеет место HasDerivAt для f(x) = x log x с производной log x + 1 в точке x.

LaTeX

$$$\text{HasDerivAt}(x \mapsto x \log x, \log x + 1, x)\quad (x \neq 0)$$$

Lean4

theorem hasDerivAt_mul_log {x : ℝ} (hx : x ≠ 0) : HasDerivAt (fun x ↦ x * log x) (log x + 1) x :=
  by
  rw [← deriv_mul_log hx, hasDerivAt_deriv_iff]
  refine DifferentiableOn.differentiableAt differentiableOn_mul_log ?_
  simp [hx]

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