map_map₂ — Mathlib

English

Mapping a function g over the result of map₂ f a b is the same as applying g to f a b inside map₂.

Русский

Постобработкой результата map₂ f a b функцией g является то же самое, что применение g к результату f внутри map₂.

LaTeX

$$$ \mathrm{map}\ g (\mathrm{map}_2 f\ a\ b) = \mathrm{map}_2 (\lambda a b. g (f a b))\ a\ b $$$

Lean4

theorem map_map₂ (f : α → β → γ) (g : γ → δ) : (map₂ f a b).map g = map₂ (fun a b => g (f a b)) a b := by grind

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