# Documentation

Mathlib.Data.List.Zip

# 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₂]).

@[simp]
theorem List.zipWith_cons_cons {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (a : α) (b : β) (l₁ : List α) (l₂ : List β) :
List.zipWith f (a :: l₁) (b :: l₂) = f a b :: List.zipWith f l₁ l₂
@[simp]
theorem List.zip_cons_cons {α : Type u} {β : Type u_1} (a : α) (b : β) (l₁ : List α) (l₂ : List β) :
List.zip (a :: l₁) (b :: l₂) = (a, b) :: List.zip l₁ l₂
@[simp]
theorem List.zipWith_nil_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l : List β) :
List.zipWith f [] l = []
theorem List.zipWith_nil_right {α : Type u} {β : Type u_2} {γ : Type u_1} (f : αβγ) (l : List α) :
List.zipWith f l [] = []
@[simp]
theorem List.zipWith_eq_nil_iff {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {l : List α} {l' : List β} :
List.zipWith f l l' = [] l = [] l' = []
@[simp]
theorem List.zip_nil_left {α : Type u} {β : Type u_1} (l : List α) :
List.zip [] l = []
@[simp]
theorem List.zip_nil_right {α : Type u} {β : Type u_1} (l : List α) :
List.zip l [] = []
@[simp]
theorem List.zip_swap {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) :
List.map Prod.swap (List.zip l₁ l₂) = List.zip l₂ l₁
@[simp]
theorem List.length_zip {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) :
List.length (List.zip l₁ l₂) = min () ()
theorem List.all₂_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {p : γProp} {l₁ : List α} {l₂ : List β} (_h : = ) :
List.All₂ p (List.zipWith f l₁ l₂) List.Forall₂ (fun x y => p (f x y)) l₁ l₂
theorem List.lt_length_left_of_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {i : } {l : List α} {l' : List β} (h : i < List.length (List.zipWith f l l')) :
i <
theorem List.lt_length_right_of_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {i : } {l : List α} {l' : List β} (h : i < List.length (List.zipWith f l l')) :
i <
theorem List.lt_length_left_of_zip {α : Type u} {β : Type u_1} {i : } {l : List α} {l' : List β} (h : i < List.length (List.zip l l')) :
i <
theorem List.lt_length_right_of_zip {α : Type u} {β : Type u_1} {i : } {l : List α} {l' : List β} (h : i < List.length (List.zip l l')) :
i <
theorem List.zip_append {α : Type u} {β : Type u_1} {l₁ : List α} {r₁ : List α} {l₂ : List β} {r₂ : List β} (_h : = ) :
List.zip (l₁ ++ r₁) (l₂ ++ r₂) = List.zip l₁ l₂ ++ List.zip r₁ r₂
theorem List.zip_map {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : αγ) (g : βδ) (l₁ : List α) (l₂ : List β) :
List.zip (List.map f l₁) (List.map g l₂) = List.map (Prod.map f g) (List.zip l₁ l₂)
theorem List.zip_map_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αγ) (l₁ : List α) (l₂ : List β) :
List.zip (List.map f l₁) l₂ = List.map (Prod.map f id) (List.zip l₁ l₂)
theorem List.zip_map_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : βγ) (l₁ : List α) (l₂ : List β) :
List.zip l₁ (List.map f l₂) = List.map (Prod.map id f) (List.zip l₁ l₂)
@[simp]
theorem List.zipWith_map {α : Type u} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : Type u_1} (f : γδμ) (g : αγ) (h : βδ) (as : List α) (bs : List β) :
List.zipWith f (List.map g as) (List.map h bs) = List.zipWith (fun a b => f (g a) (h b)) as bs
theorem List.zipWith_map_left {α : Type u} {β : Type u_2} {γ : Type u_3} {δ : Type u_1} (f : αβγ) (g : δα) (l : List δ) (l' : List β) :
List.zipWith f (List.map g l) l' = List.zipWith (f g) l l'
theorem List.zipWith_map_right {α : Type u} {β : Type u_3} {γ : Type u_2} {δ : Type u_1} (f : αβγ) (l : List α) (g : δβ) (l' : List δ) :
List.zipWith f l (List.map g l') = List.zipWith (fun x => f x g) l l'
theorem List.zip_map' {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβ) (g : αγ) (l : List α) :
List.zip (List.map f l) (List.map g l) = List.map (fun a => (f a, g a)) l
theorem List.map_zipWith {α : Type u} {β : Type u_3} {γ : Type u_2} {δ : Type u_1} (f : αβ) (g : γδα) (l : List γ) (l' : List δ) :
List.map f (List.zipWith g l l') = List.zipWith (fun x y => f (g x y)) l l'
theorem List.mem_zip {α : Type u} {β : Type u_1} {a : α} {b : β} {l₁ : List α} {l₂ : List β} :
(a, b) List.zip l₁ l₂a l₁ b l₂
theorem List.map_fst_zip {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) :
List.map Prod.fst (List.zip l₁ l₂) = l₁
theorem List.map_snd_zip {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) :
List.map Prod.snd (List.zip l₁ l₂) = l₂
@[simp]
theorem List.unzip_nil {α : Type u} {β : Type u_1} :
= ([], [])
@[simp]
theorem List.unzip_cons {α : Type u} {β : Type u_1} (a : α) (b : β) (l : List (α × β)) :
List.unzip ((a, b) :: l) = (a :: ().fst, b :: ().snd)
theorem List.unzip_eq_map {α : Type u} {β : Type u_1} (l : List (α × β)) :
= (List.map Prod.fst l, List.map Prod.snd l)
theorem List.unzip_left {α : Type u} {β : Type u_1} (l : List (α × β)) :
().fst = List.map Prod.fst l
theorem List.unzip_right {α : Type u} {β : Type u_1} (l : List (α × β)) :
().snd = List.map Prod.snd l
theorem List.unzip_swap {α : Type u} {β : Type u_1} (l : List (α × β)) :
List.unzip (List.map Prod.swap l) =
theorem List.zip_unzip {α : Type u} {β : Type u_1} (l : List (α × β)) :
List.zip ().fst ().snd = l
theorem List.unzip_zip_left {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} :
(List.unzip (List.zip l₁ l₂)).fst = l₁
theorem List.unzip_zip_right {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} (h : ) :
(List.unzip (List.zip l₁ l₂)).snd = l₂
theorem List.unzip_zip {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} (h : = ) :
List.unzip (List.zip l₁ l₂) = (l₁, l₂)
theorem List.zip_of_prod {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {lp : List (α × β)} (hl : List.map Prod.fst lp = l) (hr : List.map Prod.snd lp = l') :
lp = List.zip l l'
theorem List.map_prod_left_eq_zip {α : Type u} {β : Type u_1} {l : List α} (f : αβ) :
List.map (fun x => (x, f x)) l = List.zip l (List.map f l)
theorem List.map_prod_right_eq_zip {α : Type u} {β : Type u_1} {l : List α} (f : αβ) :
List.map (fun x => (f x, x)) l = List.zip (List.map f l) l
theorem List.zipWith_comm {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (la : List α) (lb : List β) :
List.zipWith f la lb = List.zipWith (fun b a => f a b) lb la
theorem List.zipWith_congr {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (g : αβγ) (la : List α) (lb : List β) (h : List.Forall₂ (fun a b => f a b = g a b) la lb) :
List.zipWith f la lb = List.zipWith g la lb
theorem List.zipWith_comm_of_comm {α : Type u} {β : Type u_1} (f : ααβ) (comm : ∀ (x y : α), f x y = f y x) (l : List α) (l' : List α) :
@[simp]
theorem List.zipWith_same {α : Type u} {δ : Type u_1} (f : ααδ) (l : List α) :
List.zipWith f l l = List.map (fun a => f a a) l
theorem List.zipWith_zipWith_left {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_4} {ε : Type u_3} (f : δγε) (g : αβδ) (la : List α) (lb : List β) (lc : List γ) :
List.zipWith f (List.zipWith g la lb) lc = List.zipWith3 (fun a b c => f (g a b) c) la lb lc
theorem List.zipWith_zipWith_right {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_4} {ε : Type u_3} (f : αδε) (g : βγδ) (la : List α) (lb : List β) (lc : List γ) :
List.zipWith f la (List.zipWith g lb lc) = List.zipWith3 (fun a b c => f a (g b c)) la lb lc
@[simp]
theorem List.zipWith3_same_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : ααβγ) (la : List α) (lb : List β) :
List.zipWith3 f la la lb = List.zipWith (fun a b => f a a b) la lb
@[simp]
theorem List.zipWith3_same_mid {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβαγ) (la : List α) (lb : List β) :
List.zipWith3 f la lb la = List.zipWith (fun a b => f a b a) la lb
@[simp]
theorem List.zipWith3_same_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αββγ) (la : List α) (lb : List β) :
List.zipWith3 f la lb lb = List.zipWith (fun a b => f a b b) la lb
instance List.instIsSymmOpListListZipWith {α : Type u} {β : Type u_1} (f : ααβ) [inst : IsSymmOp α β f] :
IsSymmOp (List α) (List β) ()
Equations
@[simp]
theorem List.length_revzip {α : Type u} (l : List α) :
@[simp]
theorem List.unzip_revzip {α : Type u} (l : List α) :
= (l, )
@[simp]
theorem List.revzip_map_fst {α : Type u} (l : List α) :
List.map Prod.fst () = l
@[simp]
theorem List.revzip_map_snd {α : Type u} (l : List α) :
List.map Prod.snd () =
theorem List.reverse_revzip {α : Type u} (l : List α) :
theorem List.revzip_swap {α : Type u} (l : List α) :
List.map Prod.swap () =
theorem List.get?_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l₁ : List α) (l₂ : List β) (i : ) :
List.get? (List.zipWith f l₁ l₂) i = Option.bind (Option.map f (List.get? l₁ i)) fun g => Option.map g (List.get? l₂ i)
theorem List.get?_zip_with_eq_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (l₁ : List α) (l₂ : List β) (z : γ) (i : ) :
List.get? (List.zipWith f l₁ l₂) i = some z x y, List.get? l₁ i = some x List.get? l₂ i = some y f x y = z
theorem List.get?_zip_eq_some {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) (z : α × β) (i : ) :
List.get? (List.zip l₁ l₂) i = some z List.get? l₁ i = some z.fst List.get? l₂ i = some z.snd
@[simp]
theorem List.get_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {l : List α} {l' : List β} {i : Fin (List.length (List.zipWith f l l'))} :
List.get (List.zipWith f l l') i = f (List.get l { val := i, isLt := (_ : i < ) }) (List.get l' { val := i, isLt := (_ : i < ) })
@[simp]
theorem List.nthLe_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {l : List α} {l' : List β} {i : } {h : i < List.length (List.zipWith f l l')} :
List.nthLe (List.zipWith f l l') i h = f (List.nthLe l i (_ : i < )) (List.nthLe l' i (_ : i < ))
@[simp]
theorem List.get_zip {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : Fin (List.length (List.zip l l'))} :
List.get (List.zip l l') i = (List.get l { val := i, isLt := (_ : i < ) }, List.get l' { val := i, isLt := (_ : i < ) })
@[simp]
theorem List.nthLe_zip {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : } {h : i < List.length (List.zip l l')} :
List.nthLe (List.zip l l') i h = (List.nthLe l i (_ : i < ), List.nthLe l' i (_ : i < ))
theorem List.mem_zip_inits_tails {α : Type u} {l : List α} {init : List α} {tail : List α} :
(init, tail) List.zip () () init ++ tail = l
theorem List.map_uncurry_zip_eq_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l : List α) (l' : List β) :
List.map () (List.zip l l') = List.zipWith f l l'
@[simp]
theorem List.sum_zipWith_distrib_left {α : Type u} {β : Type u_2} {γ : Type u_1} [inst : ] (f : αβγ) (n : γ) (l : List α) (l' : List β) :
List.sum (List.zipWith (fun x y => n * f x y) l l') = n * List.sum (List.zipWith f l l')

### Operations that can be applied before or after a zip_with#

theorem List.zipWith_distrib_take {α : Type u} {β : Type u_2} {γ : Type u_1} (f : αβγ) (l : List α) (l' : List β) (n : ) :
theorem List.zipWith_distrib_drop {α : Type u} {β : Type u_2} {γ : Type u_1} (f : αβγ) (l : List α) (l' : List β) (n : ) :
theorem List.zipWith_distrib_tail {α : Type u} {β : Type u_2} {γ : Type u_1} (f : αβγ) (l : List α) (l' : List β) :
theorem List.zipWith_append {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l : List α) (la : List α) (l' : List β) (lb : List β) (h : ) :
List.zipWith f (l ++ la) (l' ++ lb) = List.zipWith f l l' ++ List.zipWith f la lb
theorem List.zipWith_distrib_reverse {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l : List α) (l' : List β) (h : ) :
theorem List.sum_add_sum_eq_sum_zipWith_add_sum_drop {α : Type u} [inst : ] (L : List α) (L' : List α) :
+ List.sum L' = List.sum (List.zipWith (fun x x_1 => x + x_1) L L') + List.sum (List.drop () L) + List.sum (List.drop () L')
abbrev List.sum_add_sum_eq_sum_zipWith_add_sum_drop.match_1 {α : Type u_1} (motive : List αList αProp) :
(x x_1 : List α) → ((ys : List α) → motive [] ys) → ((xs : List α) → motive xs []) → ((x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)) → motive x x_1
Equations
• One or more equations did not get rendered due to their size.
theorem List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop {α : Type u} [inst : ] (L : List α) (L' : List α) :
* = List.prod (List.zipWith (fun x x_1 => x * x_1) L L') * List.prod (List.drop () L) * List.prod (List.drop () L')
theorem List.sum_add_sum_eq_sum_zipWith_of_length_eq {α : Type u} [inst : ] (L : List α) (L' : List α) (h : ) :
+ List.sum L' = List.sum (List.zipWith (fun x x_1 => x + x_1) L L')
theorem List.prod_mul_prod_eq_prod_zipWith_of_length_eq {α : Type u} [inst : ] (L : List α) (L' : List α) (h : ) :
* = List.prod (List.zipWith (fun x x_1 => x * x_1) L L')