image_swap_eq_preimage_swap — Mathlib

English

The image of Prod.swap equals the preimage under Prod.swap, reflecting the fact that swap is an involution on pairs.

Русский

Образ Prod.swap равен предобразу по Prod.swap, поскольку обмен координат образует взаимно однозначное отображение.

LaTeX

$$$\operatorname{image}(\mathrm{Prod.swap}) = \operatorname{preimage}(\mathrm{Prod.swap})$$$

Lean4

theorem image_swap_eq_preimage_swap : image (@Prod.swap α β) = preimage Prod.swap :=
  image_eq_preimage_of_inverse Prod.swap_leftInverse Prod.swap_rightInverse

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