English
For seq: X → Y × Z, Tendsto seq to p in 𝓝 p is equivalent to both coordinate Tendsto to p.fst and p.snd.
Русский
Для последовательности seq: X → Y × Z, сходится к 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 tendsto_iff {X} (seq : X → Y × Z) {f : Filter X} (p : Y × Z) :
Tendsto seq f (𝓝 p) ↔ Tendsto (fun n => (seq n).fst) f (𝓝 p.fst) ∧ Tendsto (fun n => (seq n).snd) f (𝓝 p.snd) := by
rw [nhds_prod_eq, Filter.tendsto_prod_iff']
