English
Let l and m be index sets and α a type. For any function v: l ⊕ m → α, consider the diagonal matrix diag(v) indexed by l ⊕ m. In the natural 2×2 block decomposition, the bottom-right block is precisely the diagonal matrix formed from the values of v on the second summand, i.e. on Sum.inr.
Русский
Пусть l и m — множества индексов, α — множество. Для любой функции v: l ⊕ m → α возьмём диагональную матрицу diag(v), индексируемую по l ⊕ m. В естественном разбиении на блоки 2×2 нижний правый блок равен диагонали, построенной из значений v на второй сумме, то есть из v(Sum.inr(i)).
LaTeX
$$$\operatorname{toBlocks}_{22}\bigl(\operatorname{diagonal}(v)\bigr) = \operatorname{diagonal}\bigl(\lambda i. v(\operatorname{inr}(i))\bigr).$$$
Lean4
@[simp]
theorem toBlocks₂₂_diagonal (v : l ⊕ m → α) : toBlocks₂₂ (diagonal v) = diagonal (fun i => v (Sum.inr i)) :=
by
unfold toBlocks₂₂
funext i j
simp only [Sum.inr.injEq, of_apply, diagonal_apply]
