ofReal — Mathlib

English

If Tendsto f l (nhds x) for real f, then Tendsto (fun a => (f a : ℂ)) l (nhds (x : ℂ)).

Русский

Если Tendsto f l (nhds x) для вещественной f, то Tendsto (f a : ℂ) в ℂ к (x : ℂ).

LaTeX

$$$\\\\operatorname{Tendsto} f \\\\ell (\\\\mathcal{N} x) \\\\Rightarrow \\\\operatorname{Tendsto} (\\\\lambda a. (f a : \\\\mathbb{C})) \\\\ell (\\\\mathcal{N}(x \\\\mathbb{C}))$$$

Lean4

theorem _root_.Filter.Tendsto.ofReal {α : Type*} {l : Filter α} {f : α → ℝ} {x : ℝ} (hf : Tendsto f l (𝓝 x)) :
    Tendsto (fun x ↦ (f x : ℂ)) l (𝓝 (x : ℂ)) :=
  tendsto_ofReal_iff.mpr hf

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