clog — Mathlib

English

If f is differentiable on a domain and maps into slitPlane, then log ∘ f is differentiable on that domain.

Русский

Если f дифференцируема на области и принимает значения в slitPlane, то log ∘ f дифференцируема на этой области.

LaTeX

$$$$ \text{If } f \text{ is differentiable on } E, \text{ and } f(E) \subseteq \mathrm{slitPlane}, \; \log \circ f \text{ is differentiable on } E. $$$$

Lean4

theorem clog {f : E → ℂ} (h₁ : Differentiable ℂ f) (h₂ : ∀ x, f x ∈ slitPlane) : Differentiable ℂ fun t => log (f t) :=
  fun x => (h₁ x).clog (h₂ x)

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