tendsto_nhds_iff — Mathlib

English

For an embedding g, Tendsto f l to y is equivalent to Tendsto (g ∘ f) l to g y.

Русский

Для вложения g, сходимость f к y эквивалентна сходимости g∘f к g(y).

LaTeX

$$$\mathrm{IsEmbedding}(g) \Rightarrow \big(\mathrm{Tendsto} f\ l\ (\mathcal{N} y) \iff \mathrm{Tendsto}(g\circ f)\ l\ (\mathcal{N}(g y))\big)$$$

Lean4

theorem tendsto_nhds_iff {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsEmbedding g) :
    Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) :=
  hg.isInducing.tendsto_nhds_iff

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