sqrt — Mathlib

English

If f is differentiable on the entire space and f(x) ≠ 0 for all x, then x ↦ √(f(x)) is differentiable on the entire space.

Русский

Если f дифференцируема на всей области и для всех x выполняется f(x) ≠ 0, то x ↦ √(f(x)) дифференцируема на всей области.

LaTeX

$$$\\text{If } \\text{Differentiable } f\\text{ and } \\forall x, f(x) \\neq 0, \\text{ then } x \\mapsto \\sqrt{f(x)} \\text{ is differentiable.}$$$

Lean4

@[fun_prop]
theorem sqrt (hf : Differentiable ℝ f) (hs : ∀ x, f x ≠ 0) : Differentiable ℝ fun y => √(f y) := fun x =>
  (hf x).sqrt (hs x)

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