English
If A: X → M_{m×n}(R) and B: X → M_{n×p}(R) are continuous, then the product A(x) B(x) is continuous in x.
Русский
Если A: X → M_{m×n}(R) и B: X → M_{n×p}(R) непрерывны, то произведение A(x) B(x) непрерывно по x.
LaTeX
$$$\\operatorname{Continuous}(A) \\to \\operatorname{Continuous}(B) \\to \\operatorname{Continuous}(x \\mapsto A(x) B(x)).$$$
Lean4
/-- For square matrices the usual `continuous_mul` can be used. -/
@[continuity, fun_prop]
theorem matrix_mul [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] {A : X → Matrix m n R}
{B : X → Matrix n p R} (hA : Continuous A) (hB : Continuous B) : Continuous fun x => A x * B x :=
continuous_matrix fun _ _ => continuous_finset_sum _ fun _ _ => (hA.matrix_elem _ _).mul (hB.matrix_elem _ _)
