map_map₂_distrib_right — Mathlib

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

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