English
A function into matrices is continuous if and only if all its entries are continuous functions; in particular, if f: X → M_{m×n}(R) has each entry f_{ij} continuous, then f is continuous.
Русский
Функция, рассчитанная в матрицы, непрерывна тогда и только тогда, когда все ее элементы непрерывны; если f: X → M_{m×n}(R) имеет каждую компоненту f_{ij}, непрерывна, то и вся функция непрерывна.
LaTeX
$$$\\Big(\\forall i,j,\\ operatorname{Continuous}(\\lambda x. f(x)_{ij})\\Big) \\Rightarrow \\operatorname{Continuous}(f).$$$
Lean4
/-- To show a function into matrices is continuous it suffices to show the coefficients of the
resulting matrix are continuous -/
@[continuity]
theorem continuous_matrix [TopologicalSpace α] {f : α → Matrix m n R} (h : ∀ i j, Continuous fun a => f a i j) :
Continuous f :=
continuous_pi fun _ => continuous_pi fun _ => h _ _
