sqrt — Mathlib

English

If f is ContDiffAt of order n at x and f(x) ≠ 0, then the function y ↦ √(f(y)) is ContDiffAt of order n at x.

Русский

Если f имеет гладкость порядка n в точке x и f(x) ≠ 0, то y ↦ √(f(y)) имеет гладкость порядка n в точке x.

LaTeX

$$$\\text{ContDiffAt}^n(\\sqrt{f})\\, x \\text{ follows from } \\text{ContDiffAt}^n(f, x) \\text{ and } f(x) \\neq 0.$$$

Lean4

@[fun_prop]
theorem sqrt (hf : ContDiffAt ℝ n f x) (hx : f x ≠ 0) : ContDiffAt ℝ n (fun y => √(f y)) x :=
  (contDiffAt_sqrt hx).comp x hf

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