clog — Mathlib

English

If f is differentiable on a set s and f(x) ∈ slitPlane for all x ∈ s, then log ∘ f is differentiable on s.

Русский

Если f гладова на множестве s и для всех x ∈ s f(x) ∈ slitPlane, то log ∘ f гладова на s.

LaTeX

$$$$ \text{If } f \text{ is differentiable on } s \text{ and } \forall x \in s,\ f(x) \in \mathrm{slitPlane}, \; \log \circ f \text{ is differentiable on } s. $$$$

Lean4

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

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