comp_map_map — Mathlib

English

The map commuting with comp: applying a map to the entries inside M before comp is the same as applying the map after performing comp on M.

Русский

Совпадение отображения, когда применяем отображение к элементам внутри M до компоновки, и когда применяем отображение после выполнения comp на M.

LaTeX

$$$ \mathrm{comp}(M.map\, (\lambda M' \to M'.map f)) = (\mathrm{comp} \, M).map \, f $$$

Lean4

theorem comp_map_map (M : Matrix I J (Matrix K L R)) (f : R → R') :
    comp I J K L _ (M.map (fun M' => M'.map f)) = (comp I J K L _ M).map f :=
  rfl

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