matrixVecCons — Mathlib

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

Похожие утверждения