map_map — Mathlib

English

Applying map g after map f is the same as mapping by the composition g ∘ f.

Русский

Применение отображения g после map f эквивалентно отображению через композицию g ∘ f.

LaTeX

$$$$ \\operatorname{map} g (\\operatorname{map} f s) = \\operatorname{map} (g \\circ f) s $$$$

Lean4

@[simp]
theorem map_map (g : β → γ) (f : α → β) (s : Multiset α) : map g (map f s) = map (g ∘ f) s :=
  Quot.inductionOn s fun _l => congr_arg _ List.map_map

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