unzip — Mathlib

English

Split a sequence of pairs into two sequences: one with all first components and one with all second components.

Русский

Разбить последовательность пар на две последовательности: первые компоненты и вторые компоненты.

LaTeX

$$$ \mathrm{unzip}(s) = (\mathrm{map}\ \mathrm{fst}\ s, \ \mathrm{map}\ \mathrm{snd}\ s).$$$

Lean4

/-- Separate a sequence of pairs into two sequences -/
def unzip (s : Seq (α × β)) : Seq α × Seq β :=
  (map Prod.fst s, map Prod.snd s)

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