Theorems · Theorem

List.comp_map

∀ {α : Type u} {β : Type v} {γ : Type w} (h : β → γ) (g : α → β) (l : List α),
  List.map (h ∘ g) l = List.map h (List.map g l)

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.

Defined in

Mathlib.Data.List.Basic

Cited by

3 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext