image_image2_antidistrib_right — Mathlib

English

Symmetric to image_image2_antidistrib_right: image g (image2 f s t) = image2 f t (s.image g).

Русский

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

LaTeX

$$$\\forall s t,\\ \\operatorname{image} g (\\operatorname{image}_2 f s t) = \\operatorname{image}_2 f t (s \\ image g)$$$

Lean4

/-- Symmetric statement to `Set.image_image2_right_anticomm`. -/
theorem image_image2_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) : (image2 f s t).image g = image2 f' t (s.image g') :=
  (image_image2_antidistrib h_antidistrib).trans <| by rw [image_id']

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