hasStrictDerivAt_log — Mathlib

English

For any x ≠ 0, the derivative of log at x is 1/x.

Русский

Для любого x ≠ 0 производная log в x равна 1/x.

LaTeX

$$$$ \\frac{d}{dx}\\log x = \\frac{1}{x} \\quad (x \\neq 0). $$$$

Lean4

theorem hasStrictDerivAt_log (hx : x ≠ 0) : HasStrictDerivAt log x⁻¹ x :=
  by
  rcases hx.lt_or_gt with hx | hx
  · convert (hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x) using 1
    · ext y; exact (log_neg_eq_log y).symm
    · field_simp
  · exact hasStrictDerivAt_log_of_pos hx

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