map_swap_product — Mathlib

English

Swapping the coordinates via the swap embedding maps t × s bijectively onto s × t.

Русский

Поменяв координаты с помощью отображения обмена, получаемо эквивалентное множество, т. е. t × s ⋅ = s × t.

LaTeX

$$$(t ×ˢ s).map ⟨\mathrm{Prod.swap}, \mathrm{Prod.swap\_injective}⟩ = s ×ˢ t$$$

Lean4

theorem map_swap_product (s : Finset α) (t : Finset β) : (t ×ˢ s).map ⟨Prod.swap, Prod.swap_injective⟩ = s ×ˢ t :=
  coe_injective <| by
    push_cast
    exact Set.image_swap_prod _ _

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