log — Mathlib

English

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

Русский

Если f дифференцируема внутри s в x и f(x) ≠ 0, с уникальной точкой внутри s, то 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) : DifferentiableWithinAt ℝ (fun x => log (f x)) s x :=
  (hf.hasFDerivWithinAt.log hx).differentiableWithinAt

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