map_map₂_right_comm — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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