sqrt — Mathlib

English

If f is differentiable at x and f(x) ≠ 0, then the function y ↦ √(f(y)) is differentiable at x.

Русский

Если f дифференцируема в точке x и f(x) ≠ 0, то y ↦ √(f(y)) дифференцируема в точке x.

LaTeX

$$$\\text{If } hf:\\text{ DifferentiableAt } \\mathbb{R} f x \\text{ and } f(x) \\neq 0, \\text{ then } \\text{DifferentiableAt } \\mathbb{R} (\\sqrt{f}) x.$$$

Lean4

@[fun_prop]
theorem sqrt (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) : DifferentiableAt ℝ (fun y => √(f y)) x :=
  (hf.hasFDerivAt.sqrt hx).differentiableAt

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