toBlock_diagonal_self — Mathlib

English

The block extraction of a diagonal matrix along identical row and column predicates yields a diagonal matrix corresponding to the same diagonal entries indexed by the subtype.

Русский

Извлечение блока из диагональной матрицы по одинаковым предикатам строк и столбцов даёт диагональную матрицу с теми же диагональными элементами, индексированными подтипом.

LaTeX

$$$\\text{toBlock}(\\text{diagonal } d)\\; p\\; p = \\text{diagonal } (\\lambda i. d(i.val))$$$

Lean4

theorem toBlock_diagonal_self (d : m → α) (p : m → Prop) :
    Matrix.toBlock (diagonal d) p p = diagonal fun i : Subtype p => d ↑i :=
  by
  ext i j
  by_cases h : i = j
  · simp [h]
  · simp [h, Subtype.val_injective.ne h]

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