derivWithin_sqrt — Mathlib

English

For differentiable f within s and with f(x) ≠ 0, the derivative within sqrt(f) satisfies derivWithin sqrt(f) = derivWithin f / (2√f).

Русский

Для дифференцируемой внутри s функции f, при f(x) ≠ 0, производная внутри sqrt(f) равна derivWithin f /(2√f).

LaTeX

$$$$ \operatorname{derivWithin}(\sqrt{f}, s, x) = \frac{\operatorname{derivWithin}(f, s, x)}{2\sqrt{f(x)}}. $$$$

Lean4

theorem derivWithin_sqrt (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) (hxs : UniqueDiffWithinAt ℝ s x) :
    derivWithin (fun x => √(f x)) s x = derivWithin f s x / (2 * √(f x)) :=
  (hf.hasDerivWithinAt.sqrt hx).derivWithin hxs

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