tendsto_ofReal_iff' — Mathlib

English

For any α, 𝕜 with [RCLike 𝕜], Tendsto (f x : 𝕜) l (nhds (x : 𝕜)) ↔ Tendsto f l (nhds x).

Русский

Для любой пары α, 𝕜 с условием [RCLike 𝕜], Tendsto (f x : 𝕜) ⇄ Tendsto f.

LaTeX

$$$\\\\operatorname{Tendsto} (f x : 𝕜) \\\\ell (\\\\mathcal{N}(x : 𝕜)) \\\\iff \\\\operatorname{Tendsto} f \\\\ell (\\\\mathcal{N}(x))$$$

Lean4

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

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