map₂_map_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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