sqrt — Mathlib

English

Let f have a Fréchet derivative f' within s at x and f(x) ≠ 0. Then the derivative of √(f) within s at x is (1/(2√(f(x)))) • f'.

Русский

Пусть у функции f есть внутри s производная Фрéше в точке x и f(x) ≠ 0. Тогда производная sqrt(f) внутри s в x равна (1/(2√(f(x)))) • f'.

LaTeX

$$$D_{s}(\\sqrt{f})(x) = \\left(\\frac{1}{2\\sqrt{f(x)}}\\right) \\cdot f'$$$

Lean4

@[fun_prop]
theorem sqrt (hf : ContDiffWithinAt ℝ n f s x) (hx : f x ≠ 0) : ContDiffWithinAt ℝ n (fun y => √(f y)) s x :=
  (contDiffAt_sqrt hx).comp_contDiffWithinAt x hf

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