log — Mathlib

English

If f is differentiable within set s at x and f(x) ≠ 0, then the derivative within s of log(f) equals the derivative within s of f divided by f(x).

Русский

Если f дифференцируема внутри множества s в точке x и f(x) ≠ 0, то производная внутри s логарифма равна производной внутри s от f, делённой на f(x).

LaTeX

$$derivWithin log f s x = derivWithin f s x / f x$$

Lean4

theorem log (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) (hxs : UniqueDiffWithinAt ℝ s x) :
    derivWithin (fun x => log (f x)) s x = derivWithin f s x / f x :=
  (hf.hasDerivWithinAt.log hx).derivWithin hxs

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