zip — Mathlib

English

Zip two weak sequences into a weak sequence of pairs: zip : WSeq α → WSeq β → WSeq (α × β).

Русский

Свести две слабые последовательности в слабую последовательность пар: zip : WSeq α → WSeq β → WSeq (α × β).

LaTeX

$$$$ \\text{zip} : \\mathrm{WSeq}\\ \\alpha \\to \\mathrm{WSeq}\\ \\beta \\to \\mathrm{WSeq}(\\alpha \\times \\beta) $$$$

Lean4

/-- Zip two weak sequences into a single sequence of pairs -/
def zip : WSeq α → WSeq β → WSeq (α × β) :=
  zipWith Prod.mk

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