sqrt — Mathlib

English

If f is ContDiff on the real line and f(x) ≠ 0 for all x, then x ↦ √(f(x)) is ContDiff on the real line.

Русский

Если f относится к ContDiff на R и f(x) ≠ 0 для всех x, то x ↦ √(f(x)) является ContDiff на R.

LaTeX

$$$\\text{ContDiff}^{n}(f) \\Rightarrow \\text{ContDiff}^{n}(\\sqrt{f})$ (whenever $f(x) \\neq 0$).$$

Lean4

@[fun_prop]
theorem sqrt (hf : ContDiff ℝ n f) (h : ∀ x, f x ≠ 0) : ContDiff ℝ n fun y => √(f y) :=
  contDiff_iff_contDiffAt.2 fun x => hf.contDiffAt.sqrt (h x)

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