map_map — Mathlib

English

Applying map with f after map with g equals map of the composition f ∘ g: map f (map g x) = map (f ∘ g) x.

Русский

Применение map с f после map c g равно map композиции f ∘ g: map f (map g x) = map (f ∘ g) x.

LaTeX

$$$ map\ f\ (map\ g\ x) = map\ (f \circ g)\ x $$$

Lean4

@[to_additive]
theorem map_map {α₁ : Type*} {g : α₁ → α} {x : FreeMonoid α₁} : map f (map g x) = map (f ∘ g) x :=
  by
  unfold map
  simp only [MonoidHom.coe_mk, OneHom.coe_mk, toList_ofList, List.map_map]

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