image_image2_antidistrib — Mathlib

English

Symmetric to image2_image_left_comm: (image2 f s t).image g = image2 f' t s.image g' under an antidistributive law.

Русский

Симметрия к антираспределению: (image2 f s t).image g = image2 f' t s.image g' при антираспределяющем законе.

LaTeX

$$$\\forall s t, (image2 f s t).image g = image2 f' t (s.image g')$$$

Lean4

theorem image_image2_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
    (image2 f s t).image g = image2 f' (t.image g₁) (s.image g₂) :=
  by
  rw [image2_swap f]
  exact image_image2_distrib fun _ _ => h_antidistrib _ _

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