snd_nhds — Mathlib

English

If f: X → Y × Z tends to p in nhds under l, then the second coordinate tends to p₂ in nhds.

Русский

Если f: X → Y × Z стремится к p в nhds по фильтру l, то вторая координата стремится к p₂ в nhds.

LaTeX

$$$\operatorname{Tendsto}(f\,l\,\mathcal{N}(p)) \Rightarrow \operatorname{Tendsto}(\lambda a: X, (f(a))_2)\,l\,\mathcal{N}(p_2)$$$

Lean4

theorem snd_nhds {X} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Tendsto f l (𝓝 p)) :
    Tendsto (fun a ↦ (f a).2) l (𝓝 <| p.2) :=
  continuousAt_snd.tendsto.comp h

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