tendsto_nhds_iff — Mathlib

English

If g is an open embedding, then Tendsto with g is equivalent to Tendsto without g up to composing with g: Tendsto f l (nhds y) ↔ Tendsto (g ∘ f) l (nhds (g y)).

Русский

Если g—открытое вложение, то переходы к окрестностям сохраняются под композиции: Tendsto f l (nhds y) ↔ Tendsto (g ∘ f) l (nhds (g y)).

LaTeX

$$$ \operatorname{Tendsto} f\ l\ (\mathcal{N}y) \iff \operatorname{Tendsto} (g\circ f)\ l\ (\mathcal{N}(gy)) $$$

Lean4

theorem tendsto_nhds_iff [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsOpenEmbedding g) :
    Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) :=
  hg.isEmbedding.tendsto_nhds_iff

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