unzip_swap — Mathlib

English

Unzipping after mapping with Prod.swap equals swapping the unzip of the original list.

Русский

Разбиение на пары после отображения Prod.swap эквивалентно развороту пары, полученной из исходного списка.

LaTeX

$$$unzip (l.map Prod.swap) = (unzip l).swap$$$

Lean4

theorem unzip_swap (l : List (α × β)) : unzip (l.map Prod.swap) = (unzip l).swap :=
  by
  simp only [unzip_eq_map, map_map]
  rfl

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