map_map — Mathlib

English

Applying first f and then g to the entries of a matrix is the same as applying g ∘ f to the entries.

Русский

Сначала к элементам матрицы применяется f, затем g; в результате получается та же матрица, что при применении g ∘ f.

LaTeX

$$$\\forall {M : Matrix m n A} {f : A \\to B} {g : B \\to C}, (M.map f).map g = M.map (g \\circ f)$$$

Lean4

theorem map_map {C : Type*} {M : Matrix m n A} {f : A → B} {g : B → C} : (M.map f).map g = M.map (g ∘ f) := by ext; rfl

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