English
Let f: α → β and g: α → Fin(n) → β be functions, and let s be a subset of α. If f and g are continuous on s, then the vector-valued function a ↦ vecCons(f(a), g(a)) is continuous on s (when viewed as a function into an (n+1)-dimensional vector of β-values).
Русский
Пусть f: α → β и g: α → Fin(n) → β; пусть s ⊆ α. Если f и g непрерывны на s, тогда функция a ↦ vecCons(f(a), g(a)) непрерывна на s (рассматривая как вектор размерности n+1 над β).
LaTeX
$$$\\forall f: \\alpha \\to \\beta,\\; \\forall g: \\alpha \\to \\mathrm{Fin}(n) \\to \\beta,\\; \\forall s \\subseteq \\alpha,\\; (\\text{ContinuousOn } f\\ s) \\land (\\text{ContinuousOn } g\\ s) \\Rightarrow \\text{ContinuousOn } (a \\mapsto \\mathrm{Matrix.vecCons}(f(a), g(a)))\\ s$$$
Lean4
theorem matrixVecCons {f : α → β} {g : α → Fin n → β} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
ContinuousOn (fun a => Matrix.vecCons (f a) (g a)) s := fun a ha => (hf a ha).matrixVecCons (hg a ha)
