clog — Mathlib

English

If f: ℂ → ℂ is differentiable and f(x) ∈ slitPlane for all x in its domain, then log∘f is differentiable on the domain.

Русский

Если f: ℂ → ℂ дифференцируема и f(x) ∈ slitPlane на всей области определения, то log ∘ f дифференцируема на этой области.

LaTeX

$$$$ \text{If } f: \mathbb{C} \to \mathbb{C} \text{ is differentiable and } f(x) \in \mathrm{slitPlane} \text{ for all } x, \; \log\circ f \text{ is differentiable.} $$$$

Lean4

theorem clog {f : E → ℂ} {s : Set E} {x : E} (h₁ : DifferentiableWithinAt ℂ f s x) (h₂ : f x ∈ slitPlane) :
    DifferentiableWithinAt ℂ (fun t => log (f t)) s x :=
  (h₁.hasFDerivWithinAt.clog h₂).differentiableWithinAt

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