matrix_vecMul — Mathlib

English

If A: X → n → R is continuous, then x ↦ replicateCol ι (A x) is continuous.

Русский

Если A: X → n → R непрерывна, то x ↦ replicateCol ι (A x) непрерывно по x.

LaTeX

$$$\\operatorname{Continuous}\\big(\\lambda x:\\,X,\\ replicateCol\\ ι\\ (A\\,x)\\big).$$$

Lean4

@[continuity, fun_prop]
theorem matrix_vecMul [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [Fintype m] {A : X → m → R}
    {B : X → Matrix m n R} (hA : Continuous A) (hB : Continuous B) : Continuous fun x => A x ᵥ* B x :=
  continuous_pi fun _i => hA.dotProduct <| continuous_pi fun _j => hB.matrix_elem _ _

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