matrix_blockDiag' — Mathlib

English

For A: X → (i) → M_{m_i×n_i}(R) continuous, then x ↦ (A(x)).blockDiag' is continuous.

Русский

Пусть A: X → (i) → M_{m_i×n_i}(R) непрерывна; тогда x ↦ A(x).blockDiag' непрерывна.

LaTeX

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

Lean4

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

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