English
If f: α → ℝ tends to x along a filter l, then √(f) tends to √x along l.
Русский
Если f: α → ℝ стремится к x по фильтру l, то √(f) стремится к √x по l.
LaTeX
$$$\\\\text{Tendsto}(f,l,\\\\mathsf{nhds}(x)) \\\\Rightarrow \\\\text{Tendsto}(\\\\lambda a, \\\\sqrt{f(a)}, l, \\\\mathsf{nhds}(\\\\sqrt{x}))$$$
Lean4
theorem sqrt {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Tendsto f l (𝓝 x)) : Tendsto (fun x => √(f x)) l (𝓝 (√x)) :=
(continuous_sqrt.tendsto _).comp h