mathlib documentation

data.list.zip

@[simp]
theorem list.zip_cons_cons {α : Type u} {β : Type v} (a : α) (b : β) (l₁ : list α) (l₂ : list β) :
(a :: l₁).zip (b :: l₂) = (a, b) :: l₁.zip l₂

@[simp]
theorem list.zip_nil_left {α : Type u} {β : Type v} (l : list α) :

@[simp]
theorem list.zip_nil_right {α : Type u} {β : Type v} (l : list α) :

@[simp]
theorem list.zip_swap {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :
list.map prod.swap (l₁.zip l₂) = l₂.zip l₁

@[simp]
theorem list.length_zip {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :
(l₁.zip l₂).length = min l₁.length l₂.length

theorem list.zip_append {α : Type u} {l₁ l₂ r₁ r₂ : list α} :
l₁.length = l₂.length(l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂

theorem list.zip_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} (f : α → γ) (g : β → δ) (l₁ : list α) (l₂ : list β) :
(list.map f l₁).zip (list.map g l₂) = list.map (prod.map f g) (l₁.zip l₂)

theorem list.zip_map_left {α : Type u} {β : Type v} {γ : Type w} (f : α → γ) (l₁ : list α) (l₂ : list β) :
(list.map f l₁).zip l₂ = list.map (prod.map f id) (l₁.zip l₂)

theorem list.zip_map_right {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) (l₁ : list α) (l₂ : list β) :
l₁.zip (list.map f l₂) = list.map (prod.map id f) (l₁.zip l₂)

theorem list.zip_map' {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : α → γ) (l : list α) :
(list.map f l).zip (list.map g l) = list.map (λ (a : α), (f a, g a)) l

theorem list.mem_zip {α : Type u} {β : Type v} {a : α} {b : β} {l₁ : list α} {l₂ : list β} :
(a, b) l₁.zip l₂a l₁ b l₂

theorem list.map_fst_zip {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :
l₁.length l₂.lengthlist.map prod.fst (l₁.zip l₂) = l₁

theorem list.map_snd_zip {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :
l₂.length l₁.lengthlist.map prod.snd (l₁.zip l₂) = l₂

@[simp]
theorem list.unzip_nil {α : Type u} {β : Type v} :

@[simp]
theorem list.unzip_cons {α : Type u} {β : Type v} (a : α) (b : β) (l : list × β)) :
((a, b) :: l).unzip = (a :: l.unzip.fst, b :: l.unzip.snd)

theorem list.unzip_eq_map {α : Type u} {β : Type v} (l : list × β)) :

theorem list.unzip_left {α : Type u} {β : Type v} (l : list × β)) :

theorem list.unzip_right {α : Type u} {β : Type v} (l : list × β)) :

theorem list.unzip_swap {α : Type u} {β : Type v} (l : list × β)) :

theorem list.zip_unzip {α : Type u} {β : Type v} (l : list × β)) :

theorem list.unzip_zip_left {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} :
l₁.length l₂.length(l₁.zip l₂).unzip.fst = l₁

theorem list.unzip_zip_right {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} :
l₂.length l₁.length(l₁.zip l₂).unzip.snd = l₂

theorem list.unzip_zip {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} :
l₁.length = l₂.length(l₁.zip l₂).unzip = (l₁, l₂)

@[simp]
theorem list.length_revzip {α : Type u} (l : list α) :

@[simp]
theorem list.unzip_revzip {α : Type u} (l : list α) :

@[simp]
theorem list.revzip_map_fst {α : Type u} (l : list α) :

@[simp]
theorem list.revzip_map_snd {α : Type u} (l : list α) :

theorem list.reverse_revzip {α : Type u} (l : list α) :

theorem list.revzip_swap {α : Type u} (l : list α) :

theorem list.nth_zip_with {α β γ : Type u_1} (f : α → β → γ) (l₁ : list α) (l₂ : list β) (i : ) :
(list.zip_with f l₁ l₂).nth i = f <$> l₁.nth i <*> l₂.nth i

theorem list.nth_zip_with_eq_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l₁ : list α) (l₂ : list β) (z : γ) (i : ) :
(list.zip_with f l₁ l₂).nth i = some z ∃ (x : α) (y : β), l₁.nth i = some x l₂.nth i = some y f x y = z

theorem list.nth_zip_eq_some {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) (z : α × β) (i : ) :
(l₁.zip l₂).nth i = some z l₁.nth i = some z.fst l₂.nth i = some z.snd

theorem list.mem_zip_inits_tails {α : Type u} {l init tail : list α} :
(init, tail) l.inits.zip l.tails init ++ tail = l