image_image₂_distrib_right — Mathlib

English

If g is a function on γ and f and g' are compatible with a right-distributive law, then (image₂ f s t).image g = image₂ f s (t.image g').

Русский

Если g действует справа и совместим с f, g', тогда образ двойного образа равен образу справа.

LaTeX

$$$\forall a,b,\ g (f a b) = f' a (g' b) \Rightarrow (\mathrm{image}_2 f\ s\ t).\mathrm{image}\ g = \mathrm{image}_2 f' s (t.\mathrm{image}\ g')$$$

Lean4

/-- Symmetric statement to `Finset.image_image₂_right_comm`. -/
theorem image_image₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) : (image₂ f s t).image g = image₂ f' s (t.image g') :=
  coe_injective <| by
    push_cast
    exact image_image2_distrib_right h_distrib

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