image_swap_product — Mathlib

English

For [DecidableEq (α × β)], the image of (t × s) under Prod.swap is s × t.

Русский

При наличии декидируемого равенства пары, образ обмена координатами из t × s равен s × t.

LaTeX

$$$ (t \timesˢ s).image Prod.swap = s \timesˢ t $$$

Lean4

@[simp]
theorem image_swap_product [DecidableEq (α × β)] (s : Finset α) (t : Finset β) : (t ×ˢ s).image Prod.swap = s ×ˢ t :=
  coe_injective <| by
    push_cast
    exact Set.image_swap_prod _ _

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