English
If A: X → M_{m×n}(R) is continuous, then each coordinate A(x)_{ij} is a continuous function of x.
Русский
Если A: X → M_{m×n}(R) непрерывна, то каждый элемент A(x)_{ij} — непрерывная функция от x.
LaTeX
$$$\\operatorname{Continuous}(A) \\Rightarrow \\forall i,j,\\ \\operatorname{Continuous}(x \\mapsto A(x)_{ij}).$$$
Lean4
theorem matrix_elem {A : X → Matrix m n R} (hA : Continuous A) (i : m) (j : n) : Continuous fun x => A x i j :=
(continuous_apply_apply i j).comp hA