log — Mathlib

English

If f is differentiableWithinAt on s at x and f x ≠ 0 with UniqueDiffWithinAt s x, then fderivWithin log ∘ f equals (f x)^{-1} • fderivWithin f s x.

Русский

Если f дифференцируема внутри s в x и f(x) ≠ 0, с UniqueDiffWithinAt, то fderivWithin( log ∘ f ) = (f x)^{-1} • fderivWithin f s x.

LaTeX

$$fderivWithin ℝ (log ∘ f) s x = (f x)^{-1} • fderivWithin ℝ f s x$$

Lean4

theorem log (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) (hxs : UniqueDiffWithinAt ℝ s x) :
    fderivWithin ℝ (fun x => log (f x)) s x = (f x)⁻¹ • fderivWithin ℝ f s x :=
  (hf.hasFDerivWithinAt.log hx).fderivWithin hxs

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