matrix_blockDiag — Mathlib

English

Let A: X → p × q → R^{m×n} be continuous; then x ↦ blockDiag(A(x)) is continuous.

Русский

Пусть A: X → p × q → R^{m×n} непрерывна; тогда x ↦ blockDiag(A(x)) непрерывна.

LaTeX

$$$\\operatorname{Continuous}(A) \\Rightarrow \\operatorname{Continuous}\\bigl(x \\mapsto \\operatorname{blockDiag}(A(x))\\bigr)$$$

Lean4

@[continuity, fun_prop]
theorem matrix_blockDiag {A : X → Matrix (m × p) (n × p) R} (hA : Continuous A) : Continuous fun x => blockDiag (A x) :=
  continuous_pi fun _i => continuous_matrix fun _j _k => hA.matrix_elem _ _

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