map₂_map_right — Mathlib

English

Let m: α → β → γ and n: β → γ. Then map₂ m f (g.map n) equals map₂ (λ a b, m a (n b)) f g.

Русский

Пусть m: α × β → γ и n: β → γ. Тогда map₂ m f (g.map n) = map₂ (λ a b, m a (n b)) f g.

LaTeX

$$$ map_2 m f (g.map n) = map_2 (\lambda a b, m a (n b)) f g $$$

Lean4

theorem map₂_map_right (m : α → γ → δ) (n : β → γ) : map₂ m f (g.map n) = map₂ (fun a b => m a (n b)) f g := by
  rw [map₂_swap, map₂_map_left, map₂_swap]

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