tendsto_nhds_iff — Mathlib

English

For g with IsInducing, Tendsto f l (nhds y) iff Tendsto (g ∘ f) l (nhds (g y)).

Русский

Для g с IsInducing имеем: Tendsto f l (nhds y) эквивалентно Tendsto (g ∘ f) l (nhds (g y)).

LaTeX

$$$\operatorname{IsInducing}(g) \Rightarrow \big( \operatorname{Tendsto}(f, l, \mathcal{N}(y)) \iff \operatorname{Tendsto}(g \circ f, l, \mathcal{N}(g(y))) \big).$$$

Lean4

theorem tendsto_nhds_iff {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsInducing g) :
    Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) := by rw [hg.nhds_eq_comap, tendsto_comap_iff]

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