sqrt — Mathlib

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

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