English
If f : Y → Z and g : Y → Fin n → Z converge to x and y respectively, then a ↦ Matrix.vecCons(f(a))(g(a)) tends to Matrix.vecCons(x)(y).
Русский
Если f: Y → Z и g: Y → Fin n → Z сходятся к x и y, то a ↦ Matrix.vecCons(f(a))(g(a)) сходится к Matrix.vecCons(x)(y).
LaTeX
$$$\\mathrm{Tendsto}(f, l, \\mathcal{nhds}(x))$ и $\\mathrm{Tendsto}(g, l, \\mathcal{nhds}(y)) \\Rightarrow \\mathrm{Tendsto}(a \\mapsto \\mathrm{Matrix.vecCons}(f(a))(g(a)), l, \\mathcal{nhds}(\\mathrm{Matrix.vecCons}(x)(y)))$$$
Lean4
theorem matrixVecCons {f : Y → Z} {g : Y → Fin n → Z} {l : Filter Y} {x : Z} {y : Fin n → Z} (hf : Tendsto f l (𝓝 x))
(hg : Tendsto g l (𝓝 y)) : Tendsto (fun a => Matrix.vecCons (f a) (g a)) l (𝓝 <| Matrix.vecCons x y) :=
hf.finCons hg
