sqrt — Mathlib

English

For x ≠ 0, HasStrictDerivAt sqrt at x holds with derivative 1/(2√x).

Русский

Для x ≠ 0, HasStrictDerivAt sqrt в точке x имеет производную 1/(2√x).

LaTeX

$$$$ \forall x \neq 0,\ HasStrictDerivAt(\sqrt{\cdot})(\frac{1}{2\sqrt{x}})(x). $$$$

Lean4

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

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