English
The image of s × t under the coordinate swap Prod.swap equals t × s; i.e., Prod.swap '' (s ×ˢ t) = t ×ˢ s.
Русский
Образ под действием Prod.swap множества s × t равен t × s; то естьProd.swap '' (s × t) = t × s.
LaTeX
$$$ \text{Prod.swap} '' (s \timesˢ t) = t \timesˢ s $$$
Lean4
@[simp]
theorem image_swap_prod (s : Set α) (t : Set β) : Prod.swap '' s ×ˢ t = t ×ˢ s := by
rw [image_swap_eq_preimage_swap, preimage_swap_prod]