image_swap_prod — Mathlib

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]

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