English
If a map m: α → β × γ tends to g × h along f, then the first projection of m tends to g: Tendsto (fun a ↦ (m a).1) f g.
Русский
Если отображение m: α → β × γ сходится к g × h по f, то первая компонента m сходится к g: Tendsto (λ a, (m a).1) f g.
LaTeX
$$$$\operatorname{Tendsto} (\lambda a. (m\,a)_{1})\; f\; g.$$$$
Lean4
/-- If a function tends to a product `g ×ˢ h` of filters, then its first component tends to
`g`. See also `Filter.Tendsto.fst_nhds` for the special case of converging to a point in a
product of two topological spaces. -/
theorem fst {h : Filter γ} {m : α → β × γ} (H : Tendsto m f (g ×ˢ h)) : Tendsto (fun a ↦ (m a).1) f g :=
tendsto_fst.comp H
