map_map — Mathlib

English

The map operation on DMatrix is functorial: composing two maps gives the same result as mapping with the composed function.

Русский

Операция отображения на DMatrix является функтором: композиция двух отображений эквивалентна отображению через композицию функций.

LaTeX

$$$ (M.map f).map g = M.map (\\lambda i j x, g (f x)) $$$

Lean4

@[simp]
theorem map_map {M : DMatrix m n α} {β : m → n → Type w} {γ : m → n → Type z} {f : ∀ ⦃i j⦄, α i j → β i j}
    {g : ∀ ⦃i j⦄, β i j → γ i j} : (M.map f).map g = M.map fun _ _ x => g (f x) := by ext; simp

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