hasDerivAt_negMulLog — Mathlib

English

If x ≠ 0, then HasDerivAt negMulLog (-log x - 1) x.

Русский

Если x ≠ 0, то имеет производную negMulLog с значением -log x - 1 в точке x.

LaTeX

$$HasDerivAt(\operatorname{negMulLog}, -\log x - 1, x) \quad (x \neq 0)$$

Lean4

theorem hasDerivAt_negMulLog {x : ℝ} (hx : x ≠ 0) : HasDerivAt negMulLog (-log x - 1) x :=
  by
  rw [← deriv_negMulLog hx, hasDerivAt_deriv_iff]
  refine DifferentiableOn.differentiableAt differentiableOn_negMulLog ?_
  simp [hx]

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