English
If f : Y → A0 and g : Y → ∀ j : Fin n, A (Fin.succ j) are such that f converges to x and g converges to y, then the combined sequence a ↦ Fin.cons(f(a), g(a)) converges to Fin.cons(x, y).
Русский
Пусть f : Y → A0 и g : Y → ∀ j : Fin n, A(Fin.succ j) сходятся к x и y соответственно; тогда a ↦ Fin.cons(f(a), g(a)) сходится к Fin.cons(x, y).
LaTeX
$$$\\mathrm{Tendsto}(a \\mapsto \\mathrm{Fin.cons}(f(a), g(a)))\\ l\\ (\\mathcal{nhds}(\\mathrm{Fin.cons}(x,y)))$ при $\\mathrm{Tendsto}(f\\,l\\mathbin{(}\\mathcal{nhds}(x)))$ и $\\mathrm{Tendsto}(g\\,l\\mathbin{(}\\mathcal{nhds}(y)))$$$
Lean4
theorem finCons {f : Y → A 0} {g : Y → ∀ j : Fin n, A j.succ} {l : Filter Y} {x : A 0} {y : ∀ j, A (Fin.succ j)}
(hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) : Tendsto (fun a => Fin.cons (f a) (g a)) l (𝓝 <| Fin.cons x y) :=
tendsto_pi_nhds.2 fun j => Fin.cases (by simpa) (by simpa using tendsto_pi_nhds.1 hg) j
