image_sdiff_product — Mathlib

English

The image of the SDiff operation on a product equals the difference: (s × t) image (uncurry (\\setminus)) = s \\ t.

Русский

Образ SDiff на произведении равен разности: (s × t) image (uncurry (\\setminus)) = s \\ t.

LaTeX

$$$ (s \\times\\! t).image (\\mathrm{uncurry}(\\setminus)) = s \\setminus t $$$

Lean4

theorem image_sdiff_product (s t : Finset α) : (s ×ˢ t).image (uncurry (· \ ·)) = s \\ t :=
  image_uncurry_product _ _ _

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