map_map₂_antidistrib — Mathlib

English

If a suitable anti-distributive condition holds: ∀ a b, n (m a b) = m' (n' b) (n'' a), then map₂ m f g = map₂ m' (g.map n') (f.map n'') after swapping arguments.

Русский

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

LaTeX

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

Lean4

theorem map_map₂_antidistrib {n : γ → δ} {m' : β' → α' → δ} {n₁ : β → β'} {n₂ : α → α'}
    (h_antidistrib : ∀ a b, n (m a b) = m' (n₁ b) (n₂ a)) : (map₂ m f g).map n = map₂ m' (g.map n₁) (f.map n₂) :=
  by
  rw [map₂_swap m]
  exact map_map₂_distrib fun _ _ => h_antidistrib _ _

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