sqrt — Mathlib

English

If f is differentiable at x and f(x) ≠ 0, then HasDerivAt sqrt(f) with derivative f'/(2√f(x)).

Русский

Если f дифференцируема в x и f(x) ≠ 0, то у sqrt(f) есть производная f'/(2√f(x)).

LaTeX

$$$$ \forall f, x, f',\ HasDerivAt f f' x \land f(x) \neq 0 \Rightarrow HasDerivAt(\sqrt{f}) \frac{f'}{2\sqrt{f(x)}} x. $$$$

Lean4

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

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