matrix_vecMulVec — Mathlib

English

If A: X → m → R is continuous and B: X → Matrix m n R is continuous, then the map x ↦ vecMulVec(A(x), B(x)) is continuous.

Русский

Если A: X → m → R непрерывна и B: X → Matrix m n R непрерывна, то отображение x ↦ vecMulVec(A(x), B(x)) непрерывно.

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem matrix_vecMulVec [Mul R] [ContinuousMul R] {A : X → m → R} {B : X → n → R} (hA : Continuous A)
    (hB : Continuous B) : Continuous fun x => vecMulVec (A x) (B x) :=
  continuous_matrix fun _ _ => ((continuous_apply _).comp hA).mul ((continuous_apply _).comp hB)

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