cpow_const — Mathlib

English

Let f: s → ℂ be differentiable on s and c ∈ ℂ with f(x) ∈ slitPlane for all x ∈ s. Then the map x ↦ f(x)^{c} is differentiable on s.

Русский

Пусть f: s → ℂ дифференцируема на s и f(x) ∈ разрезанная плоскость для всех x ∈ s. Тогда x ↦ f(x)^{c} дифференцируема на s.

LaTeX

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

Lean4

@[fun_prop]
theorem cpow_const (hf : DifferentiableOn ℂ f s) (h0 : ∀ x ∈ s, f x ∈ slitPlane) :
    DifferentiableOn ℂ (fun x => f x ^ c) s :=
  hf.cpow (differentiableOn_const c) h0

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