matrixVecCons — Mathlib

English

If f: X → Z and g: X → Fin n → Z are continuous at x, then a ↦ Matrix.vecCons(f(a))(g(a)) is continuous at x.

Русский

Пусть f: X → Z и g: X → Fin n → Z непрерывны в x; тогда a ↦ Matrix.vecCons(f(a))(g(a)) непрерывна в x.

LaTeX

$$$\\text{ContinuousAt } f\\ x \\land \\text{ContinuousAt } g\\ x \\Rightarrow \\text{ContinuousAt}(a \\mapsto \\mathrm{Matrix.vecCons}(f(a))(g(a)))\\ x$$$

Lean4

theorem matrixVecCons {f : X → Z} {g : X → Fin n → Z} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
    ContinuousAt (fun a => Matrix.vecCons (f a) (g a)) x :=
  hf.finCons hg

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