matrix_blockDiagonal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem matrix_blockDiagonal [Zero R] [DecidableEq p] {A : X → p → Matrix m n R} (hA : Continuous A) :
    Continuous fun x => blockDiagonal (A x) :=
  continuous_matrix fun ⟨i₁, i₂⟩ ⟨j₁, _j₂⟩ =>
    (((continuous_apply i₂).comp hA).matrix_elem i₁ j₁).if_const _ continuous_zero

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