log — Mathlib

English

If f is differentiable on s and f x ≠ 0, then log ∘ f is differentiable on s.

Русский

Если f дифференцируема на s и f(x) ≠ 0, то log ∘ f дифференцируема на s.

LaTeX

$$DifferentiableWithinAt Real f s x → Ne (f x) 0 → DifferentiableWithinAt Real (log ∘ f) s x$$

Lean4

@[fun_prop]
theorem log (hf : DifferentiableOn ℝ f s) (hx : ∀ x ∈ s, f x ≠ 0) : DifferentiableOn ℝ (fun x => log (f x)) s :=
  fun x h => (hf x h).log (hx x h)

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