const_cpow — Mathlib

English

If f: s → ℂ is differentiable on s and for all x ∈ s we have f(x) ∈ slitPlane, then x ↦ f(x)^{c} is differentiable on s for any fixed c ∈ ℂ.

Русский

Если f: s → ℂ дифференцируема на s и для всех x ∈ s имеет место f(x) ∈ slitPlane, то x ↦ f(x)^{c} дифференцируема на s для любого фиксированного c ∈ ℂ.

LaTeX

$$$\\text{Let }f:s\\to\\mathbb{C}\\text{ be differentiable on }s\\text{ and }\\forall x\\in s,\\ f(x)\\in\\mathrm{slitPlane}. \\\\ \\text{Then } x\\mapsto f(x)^{c}\\text{ is differentiable on }s.$$$

Lean4

@[fun_prop]
theorem const_cpow (hf : Differentiable ℂ f) (h0 : c ≠ 0 ∨ ∀ x, f x ≠ 0) : Differentiable ℂ (fun x ↦ c ^ f x) := fun x ↦
  (hf x).const_cpow (h0.imp_right fun h ↦ h x)

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