English
For a sequence seq : X → Y × Z, Tendsto seq f (nhds p) is equivalent to Tendsto of the first and second coordinates separately to nhds p.fst and nhds p.snd.
Русский
Для последовательности seq : X → Y × Z схождение seq к p в 𝓝 p эквивалентно сходимости по первым и вторым координатам к 𝓝 p.fst и 𝓝 p.snd.
LaTeX
$$$ \\mathrm{Tendsto}\\ seq\\ f\\ (\\mathcal{N} p) \\iff \\mathrm{Tendsto}\\ (\\\\lambda n. (seq n).fst)\\ f\\ (\\mathcal{N} p.fst) \\land \\mathrm{Tendsto}\\ (\\\\lambda n. (seq n).snd)\\ f\\ (\\mathcal{N} p.snd) $$$
Lean4
theorem prodMap_nhds {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W} (hf : Tendsto f (𝓝 x) (𝓝 y))
(hg : Tendsto g (𝓝 z) (𝓝 w)) : Tendsto (Prod.map f g) (𝓝 (x, z)) (𝓝 (y, w)) :=
by
rw [nhds_prod_eq, nhds_prod_eq]
exact hf.prodMap hg
