map_map — Mathlib

English

Composing maps on entries yields a matrix equal to mapping with the composed function: (M.map f).map g = M.map (g ∘ f).

Русский

Сочетание отображений на элементах матрицы эквивалентно применению композиции функций: (M.map f).map g = M.map (g ∘ f).

LaTeX

$$$(M.map\\ f).map\\ g = M.map (g \\circ f)$$$

Lean4

@[simp]
theorem map_map {M : Matrix m n α} {β γ : Type*} {f : α → β} {g : β → γ} : (M.map f).map g = M.map (g ∘ f) :=
  by
  ext
  rfl

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