map₂_left_comm — Mathlib

English

A left-commutation form of map₂: if h_left_comm holds, then map₂ f a (map₂ g b c) equals map₂ g' b (map₂ f' a c).

Русский

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

LaTeX

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

Lean4

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

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