image₂_left_comm — Mathlib

English

Repeat of the four-way distributive commutation: image₂ f (image₂ g s t) (image₂ h u v) = image₂ f' (image₂ g' s u) (image₂ h' t v) under the corresponding hypothesis.

Русский

Повторение четырехуровневой коммутативности образа₂.

LaTeX

$$$\text{(same as 95402 with the same assumptions)}$$$

Lean4

theorem image₂_left_comm {γ : Type*} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε}
    (h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) : image₂ f s (image₂ g t u) = image₂ g' t (image₂ f' s u) :=
  coe_injective <| by
    push_cast
    exact image2_left_comm h_left_comm

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