sqrt — Mathlib

English

If f is ContDiffOn on s and f(x) ≠ 0 for all x in s, then the function y ↦ √(f(y)) is ContDiffOn on s.

Русский

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

LaTeX

$$$\\text{ContDiffOn}^{n}(\\sqrt{f}) s\\;\\;\\text{from } \\text{ContDiffOn}^{n}(f) s \\text{ and } f(x) \\neq 0\\;\\forall x\\in s.$$$

Lean4

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

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