image2_image_left_anticomm — Mathlib

English

Variant form: image g (image2 f s t) = image2 f t (s.image g) under a right-antidistributive law.

Русский

Вариант: image g (image2 f s t) = image2 f t (s.image g) при правом антираспределении.

LaTeX

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

Lean4

/-- Symmetric statement to `Set.image_image2_antidistrib_left`. -/
theorem image2_image_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
    (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) : image2 f (s.image g) t = (image2 f' t s).image g' :=
  (image_image2_antidistrib_left fun a b => (h_left_anticomm b a).symm).symm

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