English
Let A, B, C, D be blocks of compatible sizes forming the block matrix fromBlocks A B C D. Then applying a function f entrywise to the whole block matrix is the same as applying f to each block separately: (fromBlocks A B C D).map f = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f).
Русский
Пусть A, B, C, D — блоки совместимых размеров, образующие блочную матрицу M = fromBlocks A B C D. Применение к M поэлементно функции f эквивалентно применению f к каждому блоку: (fromBlocks A B C D).map f = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f).
LaTeX
$$$ (\\text{fromBlocks } A \\ B \\ C \\ D).map f = \\text{fromBlocks } (A.map f) (B.map f) (C.map f) (D.map f) $$$
Lean4
theorem fromBlocks_map (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : α → β) :
(fromBlocks A B C D).map f = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) := by ext i j;
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]
