sqrt — Mathlib

English

If f is differentiable within a set s at x and f(x) ≠ 0, then the composition y ↦ √(f(y)) is differentiable within s at x.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem sqrt (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) : DifferentiableWithinAt ℝ (fun y => √(f y)) s x :=
  (hf.hasFDerivWithinAt.sqrt hx).differentiableWithinAt

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