English
If f and g are ContinuousWithinAt on s, then the combined map a ↦ Matrix.vecCons(f(a), g(a)) is ContinuousWithinAt on s.
Русский
Если f и g непрерывны внутри на s, то отображение a ↦ Matrix.vecCons(f(a), g(a)) непрерывно внутри на s.
LaTeX
$$$$\text{ContinuousWithinAt }f\ s\ a \land \text{ContinuousWithinAt }g\ s\ a \Rightarrow \text{ContinuousWithinAt }\bigl(a \mapsto \mathrm{Matrix.vecCons}(f(a), g(a))\bigr)\ s\ a.$$$$
Lean4
theorem matrixVecCons {f : α → β} {g : α → Fin n → β} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a)
(hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun a => Matrix.vecCons (f a) (g a)) s a :=
hf.tendsto.matrixVecCons hg