map₂_map_right — Mathlib

English

Applying map to the right argument before map₂ is equivalent to mapping the transformed right argument inside map₂.

Русский

Применение map к правому аргументу до map₂ эквивалентно отображению преобразованного правого аргумента внутри map₂.

LaTeX

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

Lean4

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

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