matrix_blockDiagonal' — Mathlib

English

For A: X → ∀ i, M_{m_i×n_i}(R) continuous, the blockDiagonal' mapping is continuous.

Русский

Пусть A: X → ∀ i, M_{m_i×n_i}(R) непрерывна; тогда blockDiagonal'(A(x)) непрерывна по 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 l] {A : X → ∀ i, Matrix (m' i) (n' i) R} (hA : Continuous A) :
    Continuous fun x => blockDiagonal' (A x) :=
  continuous_matrix fun ⟨i₁, i₂⟩ ⟨j₁, j₂⟩ =>
    by
    dsimp only [blockDiagonal'_apply']
    split_ifs with h
    · subst h
      exact ((continuous_apply i₁).comp hA).matrix_elem i₂ j₂
    · exact continuous_const

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