sqrt — Mathlib

English

If f is differentiable on a set s and f(x) ≠ 0 for all x ∈ s, then x ↦ √(f(x)) is differentiable on s.

Русский

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

LaTeX

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

Lean4

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

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