map_map₂_antidistrib_left — Mathlib

English

Symmetric version of anti-distributivity on the right: if ∀ a b, m a (n b) = n' (m' b a), then map₂ m f (g.map n) = (map₂ m' g f).map n'.

Русский

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

LaTeX

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

Lean4

/-- Symmetric statement to `Filter.map₂_map_left_anticomm`. -/
theorem map_map₂_antidistrib_left {n : γ → δ} {m' : β' → α → δ} {n' : β → β'}
    (h_antidistrib : ∀ a b, n (m a b) = m' (n' b) a) : (map₂ m f g).map n = map₂ m' (g.map n') f :=
  map_map₂_antidistrib h_antidistrib

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