toBlocks₁₁_diagonal — Mathlib

English

Taking the top-left sub-blocks of the diagonal matrix results in a diagonal matrix whose diagonal is the restriction of v to the left summand.

Русский

Верхняя левая часть диагональной матрицы снова диагональная и имеет диагональ, равную ограничению в на левом суммировании.

LaTeX

$$$ toBlocks_{11} (\\text{diagonal } v) = \\text{diagonal } (v \\circ \\mathrm{Sum.inl}) $$$

Lean4

@[simp]
theorem toBlocks₁₁_diagonal (v : l ⊕ m → α) : toBlocks₁₁ (diagonal v) = diagonal (fun i => v (Sum.inl i)) :=
  by
  unfold toBlocks₁₁
  funext i j
  simp only [Sum.inl.injEq, of_apply, diagonal_apply]

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