map₂_map_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map₂_map_left (m : γ → β → δ) (n : α → γ) : map₂ m (f.map n) g = map₂ (fun a b => m (n a) b) f g := by
  rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, ← @map_id _ g, prod_map_map_eq, map_map, map_id]; rfl

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