map_map₂_distrib_left — Mathlib

English

Symmetric left-distributivity under the same hypotheses.

Русский

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

LaTeX

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

Lean4

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

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