tendsto_ofReal_iff — Mathlib

English

For α, l, f: α → ℝ, x ∈ ℝ, Tendsto (f) l (nhds x) iff Tendsto (fun a ↦ (f a : 𝕜)) l (nhds x).

Русский

Пределы переводятся через отображение Real → 𝕜: эквивалентно Tendsto реального и комплексного вариантов.

LaTeX

$$$\\\\operatorname{Tendsto} (\\\\lambda a \\,\\\\mapsto \\\\overline{f(a)} )\, l \\, (\\\\mathcal{N}(x \\\\mathbb{C})) \\\\iff \\\\operatorname{Tendsto} f \\, l \\, (\\\\mathcal{N}(x))$$$

Lean4

theorem _root_.Filter.tendsto_ofReal_iff {α : Type*} {l : Filter α} {f : α → ℝ} {x : ℝ} :
    Tendsto (fun x ↦ (f x : ℂ)) l (𝓝 (x : ℂ)) ↔ Tendsto f l (𝓝 x) :=
  isUniformEmbedding_ofReal.isClosedEmbedding.tendsto_nhds_iff.symm

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