English
Symmetric to the right distributive law: (map₂ m f g).map n = map₂ m' f (g.map n') under ∀ a b, n (m a b) = m' a (n' b).
Русский
Симметрично правой версии: (map₂ m f g).map n = map₂ m' f (g.map n') при условии ∀ a b, n (m a b) = m' a (n' b).
LaTeX
$$$\mathrm{map}\,(\mathrm{map}_2\,m\,f\,g) = \mathrm{map}_2 m'\,f\,(g.map\,n')$
\text{при } \forall a b, n (m a b) = m' a (n' b)$$
Lean4
/-- Symmetric statement to `Filter.map_map₂_right_comm`. -/
theorem map_map₂_distrib_right {n : γ → δ} {m' : α → β' → δ} {n' : β → β'}
(h_distrib : ∀ a b, n (m a b) = m' a (n' b)) : (map₂ m f g).map n = map₂ m' f (g.map n') :=
map_map₂_distrib h_distrib