# zip & unzip #

This file provides results about `List.zipWith`, `List.zip` and `List.unzip` (definitions are in core Lean). `zipWith f l₁ l₂` applies `f : α → β → γ` pointwise to a list `l₁ : List α` and `l₂ : List β`. It applies, until one of the lists is exhausted. For example, `zipWith f [0, 1, 2] [6.28, 31] = [f 0 6.28, f 1 31]`. `zip` is `zipWith` applied to `Prod.mk`. For example, `zip [a₁, a₂] [b₁, b₂, b₃] = [(a₁, b₁), (a₂, b₂)]`. `unzip` undoes `zip`. For example, `unzip [(a₁, b₁), (a₂, b₂)] = ([a₁, a₂], [b₁, b₂])`.

source
@[simp]
theorem List.zip_swap {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) :
map Prod.swap (l₁.zip l₂) = l₂.zip l₁
source
theorem List.forall_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {p : γ → Prop} {l₁ : List α} {l₂ : List β} :
l₁.length = l₂.length → (Forall p (zipWith f l₁ l₂) ↔ Forall₂ (fun (x : α) (y : β) => p (f x y)) l₁ l₂)
source
theorem List.unzip_swap {α : Type u} {β : Type u_1} (l : List (α × β)) :
(map Prod.swap l).unzip = l.unzip.swap
source
theorem List.zipWith_congr {α : Type u} {β : Type u_1} {γ : Type u_2} (f g : α → β → γ) (la : List α) (lb : List β) (h : Forall₂ (fun (a : α) (b : β) => f a b = g a b) la lb) :
zipWith f la lb = zipWith g la lb
source
theorem List.zipWith_zipWith_left {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {ε : Type u_4} (f : δ → γ → ε) (g : α → β → δ) (la : List α) (lb : List β) (lc : List γ) :
zipWith f (zipWith g la lb) lc = zipWith3 (fun (a : α) (b : β) (c : γ) => f (g a b) c) la lb lc
source
theorem List.zipWith_zipWith_right {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {ε : Type u_4} (f : α → δ → ε) (g : β → γ → δ) (la : List α) (lb : List β) (lc : List γ) :
zipWith f la (zipWith g lb lc) = zipWith3 (fun (a : α) (b : β) (c : γ) => f a (g b c)) la lb lc
source
@[simp]
theorem List.zipWith3_same_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → α → β → γ) (la : List α) (lb : List β) :
zipWith3 f la la lb = zipWith (fun (a : α) (b : β) => f a a b) la lb
source
@[simp]
theorem List.zipWith3_same_mid {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → α → γ) (la : List α) (lb : List β) :
zipWith3 f la lb la = zipWith (fun (a : α) (b : β) => f a b a) la lb
source
@[simp]
theorem List.zipWith3_same_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → β → γ) (la : List α) (lb : List β) :
zipWith3 f la lb lb = zipWith (fun (a : α) (b : β) => f a b b) la lb
source
instance List.instIsSymmOpZipWith {α : Type u} {β : Type u_1} (f : α → α → β) [IsSymmOp f] :
IsSymmOp (zipWith f)
source
@[simp]
theorem List.length_revzip {α : Type u} (l : List α) :
l.revzip.length = l.length
source
@[simp]
theorem List.unzip_revzip {α : Type u} (l : List α) :
l.revzip.unzip = (l, l.reverse)
source
@[simp]
theorem List.revzip_map_fst {α : Type u} (l : List α) :
map Prod.fst l.revzip = l
source
@[simp]
theorem List.revzip_map_snd {α : Type u} (l : List α) :
map Prod.snd l.revzip = l.reverse
source
theorem List.reverse_revzip {α : Type u} (l : List α) :
l.revzip.reverse = l.reverse.revzip
source
theorem List.revzip_swap {α : Type u} (l : List α) :
map Prod.swap l.revzip = l.reverse.revzip
source
theorem List.mem_zip_inits_tails {α : Type u} {l init tail : List α} :
(init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l