English
For any h: β → γ, g: α → β, and l: List α, map (h ∘ g) l = map h (map g l).
Русский
Для любых h: β → γ, g: α → β и l: List α выполняется map (h ∘ g) l = map h (map g l).
LaTeX
$$$\\\\forall {f:\\\\beta \\\\to \\\\gamma} {g:\\\\alpha \\\\to \\\\beta} {l:\\\\text{List }\\\\alpha}, \\\\operatorname{map}(f \\\\circ g)\ l = \\\\operatorname{map} f (\\\\operatorname{map} g\ l).$$$
Lean4
/-- A single `List.map` of a composition of functions is equal to
composing a `List.map` with another `List.map`, fully applied.
This is the reverse direction of `List.map_map`.
-/
theorem comp_map (h : β → γ) (g : α → β) (l : List α) : map (h ∘ g) l = map h (map g l) :=
map_map.symm
