sqrt — Mathlib

English

If f is differentiable within a set and f(x) ≠ 0, then HasDerivWithinAt sqrt(f) with the usual quotient form.

Русский

Если f определена внутри множества и f(x) ≠ 0, то sqrt(f) имеет производную внутри множества по обычной формуле.

LaTeX

$$$$ \forall f, s, x,\ HasDerivWithinAt f\ f'\ s\ x \implies\ Ne\, f(x)\ 0 \rightarrow\ HasDerivWithinAt(\sqrt{f})\ \frac{f'}{2\sqrt{f(x)}}\ s\ x. $$$$

Lean4

theorem sqrt (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0) :
    HasDerivWithinAt (fun y => √(f y)) (f' / (2 * √(f x))) s x := by
  simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasDerivAt_sqrt hx).comp_hasDerivWithinAt x hf

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