English
If f is differentiable within s at x and f(x) ≠ 0 and the differentiation is unique within s at x, then the derivative of √(f) within s at x equals (1/(2√(f(x)))) • fderivWithin f s x.
Русский
Если f дифференцируема внутри s в точке x и f(x) ≠ 0, и существует уникальная производная внутри s в x, то fderivWithin(√(f)) s x = (1/(2√(f(x)))) • fderivWithin f s x.
LaTeX
$$$fderivWithin\\Big( \\sqrt{f} \\Big)\\, s\\, x = \\left(\\frac{1}{2 \\sqrt{f(x)}}\\right) \\cdot fderivWithin\\, f\\, s\\, x$$$
Lean4
theorem fderivWithin_sqrt (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) (hxs : UniqueDiffWithinAt ℝ s x) :
fderivWithin ℝ (fun x => √(f x)) s x = (1 / (2 * √(f x))) • fderivWithin ℝ f s x :=
(hf.hasFDerivWithinAt.sqrt hx).fderivWithin hxs
