English
If A, B, C, D are continuous matrix-valued functions, then the block matrix formed by them is a continuous function.
Русский
Если A, B, C, D — непрерывные функции матриц, то матрица из блоков непрерывна.
LaTeX
$$$\\operatorname{Continuous}(A) \\land \\operatorname{Continuous}(B) \\land \\operatorname{Continuous}(C) \\land \\operatorname{Continuous}(D) \\Rightarrow \\operatorname{Continuous}\\bigl(x \\mapsto \\operatorname{fromBlocks}(A(x),B(x),C(x),D(x))\\bigr)$$$
Lean4
@[continuity, fun_prop]
theorem matrix_fromBlocks {A : X → Matrix n l R} {B : X → Matrix n m R} {C : X → Matrix p l R} {D : X → Matrix p m R}
(hA : Continuous A) (hB : Continuous B) (hC : Continuous C) (hD : Continuous D) :
Continuous fun x => Matrix.fromBlocks (A x) (B x) (C x) (D x) :=
continuous_matrix <| by rintro (i | i) (j | j) <;> refine Continuous.matrix_elem ?_ i j <;> assumption
