snd — Mathlib

English

If m tends to g × h along f, then the second projection tends to h: Tendsto (fun a ↦ (m a).2) f h.

Русский

Если отображение m сходится к g × h по f, тогда вторая компонента m сходится к h.

LaTeX

$$$$\operatorname{Tendsto} (\lambda a. (m\,a)_{2})\; f\; h.$$$$

Lean4

/-- If a function tends to a product `g ×ˢ h` of filters, then its second component tends to
`h`. See also `Filter.Tendsto.snd_nhds` for the special case of converging to a point in a
product of two topological spaces. -/
theorem snd {h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g ×ˢ h)) : Tendsto (fun a ↦ (m a).2) f h :=
  tendsto_snd.comp H

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