zip — Mathlib

English

Pair two sequences into a sequence of coordinatewise pairs: the i-th element is (a_i,b_i).

Русский

Соединить две последовательности в последовательность пар по координатам: i-й элемент есть (a_i,b_i).

LaTeX

$$$ \text{zip} : \mathrm{Seq}(\alpha) \to \mathrm{Seq}(\beta) \to \mathrm{Seq}(\alpha \times \beta),\quad \text{zip}(s,t) = \text{zipWith}(\mathrm{Prod.mk})(s,t).$$$

Lean4

/-- Pair two sequences into a sequence of pairs -/
def zip : Seq α → Seq β → Seq (α × β) :=
  zipWith Prod.mk

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