cpow_const — Mathlib

English

If f is differentiable within s, then x ↦ f(x)^c is differentiable within s for fixed c if f(x) ∈ slitPlane.

Русский

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

LaTeX

$$$\\\\forall f, s, x, c, DifferentiableWithinAt \\mathbb{C} f s x \\\\Rightarrow DifferentiableWithinAt \\mathbb{C} (\\\\lambda x, f(x)^c) s x$$$

Lean4

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

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