cpow_const — Mathlib

English

If f is differentiable at x, then f(x)^c is differentiable at x for fixed c with f(x) ∈ slitPlane.

Русский

Если f дифференцируема в x, то f(x)^c дифференцируема в x при фиксированном c и f(x) ∈ slitPlane.

LaTeX

$$$\\\\forall f, x, c, \\text{DifferentiableAt } f x \\\\Rightarrow \\text{DifferentiableAt } (\\lambda z, f(z)^c) x$$$

Lean4

@[fun_prop]
theorem cpow_const (hf : DifferentiableAt ℂ f x) (h0 : f x ∈ slitPlane) : DifferentiableAt ℂ (fun x => f x ^ c) x :=
  hf.cpow (differentiableAt_const c) h0

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