sqrt — Mathlib

English

If f is ContinuousWithinAt on s at x, then the function a ↦ √(f(a)) is ContinuousWithinAt on s at x.

Русский

Если f непрерывна на отрезке s в точке x, то a ↦ √(f(a)) непрерывна на s в x.

LaTeX

$$$\\\\text{ContinuousWithinAt}(f,s,x) \\\\Rightarrow \\\\text{ContinuousWithinAt}(\\\\lambda z, \\\\sqrt{f(z)}, s, x)$$$

Lean4

nonrec theorem sqrt (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => √(f x)) s x :=
  h.sqrt

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