map_comp_map — Mathlib

English

Composing a List.map with another List.map yields a single List.map of the composed functions.

Русский

Сочетание двух отображений списка через List.map даёт одно отображение списка от композиции функций.

LaTeX

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

Lean4

/-- Composing a `List.map` with another `List.map` is equal to
a single `List.map` of composed functions.
-/
@[simp]
theorem map_comp_map (g : β → γ) (f : α → β) : map g ∘ map f = map (g ∘ f) := by ext l;
  rw [comp_map, Function.comp_apply]

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