map₂_right_comm — Mathlib

English

A right-commutation form of map₂: if h_right_comm holds, then map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b.

Русский

Правая форма коммутативности map₂: если выполнено h_right_comm, тогда map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b.

LaTeX

$$$ \forall a b c,\; f (g a b) c = g' (f' a c) b \Rightarrow \mathrm{map}_2 f (\mathrm{map}_2 g a b) c = \mathrm{map}_2 g' (\mathrm{map}_2 f' a c) b $$$

Lean4

theorem map₂_right_comm {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε}
    (h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) : map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b := by grind

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