matrixVecCons — Mathlib

English

If f and g are continuous, then a ↦ Matrix.vecCons (f(a)) (g(a)) is continuous.

Русский

Если f и g непрерывны, то a ↦ Matrix.vecCons(f(a))(g(a)) непрерывна.

LaTeX

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

Lean4

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

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