map₂_map_left_comm — Mathlib

English

Symmetric to left distributive law: if ∀ a b, m (n a) b = n' (m' a b) then map₂ m (f.map n) g = (map₂ m' f g).map n'.

Русский

Симметрично левой версии: если ∀ a b, m (n a) b = n' (m' a b), то map₂ m (f.map n) g = (map₂ m' f g).map n'.

LaTeX

$$$\mathrm{map}_2\ m\ (\mathrm{f.map}\ n)\ g = (\mathrm{map}_2\ m'\ f\ g).\mathrm{map}\ n'$$$

Lean4

/-- Symmetric statement to `Filter.map_map₂_distrib_left`. -/
theorem map₂_map_left_comm {m : α' → β → γ} {n : α → α'} {m' : α → β → δ} {n' : δ → γ}
    (h_left_comm : ∀ a b, m (n a) b = n' (m' a b)) : map₂ m (f.map n) g = (map₂ m' f g).map n' :=
  (map_map₂_distrib_left fun a b => (h_left_comm a b).symm).symm

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