log — Mathlib

English

If f is differentiable on a domain and f x ≠ 0 everywhere, then log ∘ f is differentiable on that domain.

Русский

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

LaTeX

$$Differentiable Real f → (∀ x, f x ≠ 0) → Differentiable (log ∘ f)$$

Lean4

@[simp, fun_prop]
theorem log (hf : Differentiable ℝ f) (hx : ∀ x, f x ≠ 0) : Differentiable ℝ fun x => log (f x) := fun x =>
  (hf x).log (hx x)

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