mathlib documentation

data.list.zip

@[simp]
theorem list.zip_with_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : α) (b : β) (l₁ : list α) (l₂ : list β) :
list.zip_with f (a :: l₁) (b :: l₂) = f a b :: list.zip_with f l₁ l₂
@[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_with_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : list β) :
@[simp]
theorem list.zip_with_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : list α) :
@[simp]
theorem list.zip_with_eq_nil_iff {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {l : list α} {l' : list β} :
@[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_with {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l₁ : list α) (l₂ : list β) :
(list.zip_with f l₁ l₂).length = min l₁.length l₂.length
@[simp]
theorem list.length_zip {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :
(l₁.zip l₂).length = min l₁.length l₂.length
theorem list.lt_length_left_of_zip_with {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {i : } {l : list α} {l' : list β} (h : i < (list.zip_with f l l').length) :
i < l.length
theorem list.lt_length_right_of_zip_with {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {i : } {l : list α} {l' : list β} (h : i < (list.zip_with f l l').length) :
i < l'.length
theorem list.lt_length_left_of_zip {α : Type u} {β : Type v} {i : } {l : list α} {l' : list β} (h : i < (l.zip l').length) :
i < l.length
theorem list.lt_length_right_of_zip {α : Type u} {β : Type v} {i : } {l : list α} {l' : list β} (h : i < (l.zip l').length) :
i < l'.length
theorem list.zip_append {α : Type u} {β : Type v} {l₁ r₁ : list α} {l₂ r₂ : list β} (h : 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₂)
@[simp]
theorem list.zip_with_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} {μ : Type u_1} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (as : list α) (bs : list β) :
list.zip_with f (list.map g as) (list.map h bs) = list.zip_with (λ (a : α) (b : β), f (g a) (h b)) as bs
theorem list.zip_with_map_left {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} (f : α → β → γ) (g : δ → α) (l : list δ) (l' : list β) :
list.zip_with f (list.map g l) l' = list.zip_with (f g) l l'
theorem list.zip_with_map_right {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} (f : α → β → γ) (l : list α) (g : δ → β) (l' : list δ) :
list.zip_with f l (list.map g l') = list.zip_with (λ (x : α), f x g) l 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.map_zip_with {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (f : α → β) (g : γ → δ → α) (l : list γ) (l' : list δ) :
list.map f (list.zip_with g l l') = list.zip_with (λ (x : γ) (y : δ), f (g x y)) l 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 β} (h : l₂.length l₁.length) :
(l₁.zip l₂).unzip.snd = l₂
theorem list.unzip_zip {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} (h : l₁.length = l₂.length) :
(l₁.zip l₂).unzip = (l₁, l₂)
theorem list.zip_of_prod {α : Type u} {β : Type v} {l : list α} {l' : list β} {lp : list × β)} (hl : list.map prod.fst lp = l) (hr : list.map prod.snd lp = l') :
lp = l.zip l'
theorem list.map_prod_left_eq_zip {α : Type u} {β : Type v} {l : list α} (f : α → β) :
list.map (λ (x : α), (x, f x)) l = l.zip (list.map f l)
theorem list.map_prod_right_eq_zip {α : Type u} {β : Type v} {l : list α} (f : α → β) :
list.map (λ (x : α), (f x, x)) l = (list.map f l).zip 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} {β : Type v} {γ : Type w} (f : α → β → γ) (l₁ : list α) (l₂ : list β) (i : ) :
(list.zip_with f l₁ l₂).nth i = (option.map f (l₁.nth i)).bind (λ (g : β → γ), option.map g (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
@[simp]
theorem list.nth_le_zip_with {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {l : list α} {l' : list β} {i : } {h : i < (list.zip_with f l l').length} :
(list.zip_with f l l').nth_le i h = f (l.nth_le i _) (l'.nth_le i _)
@[simp]
theorem list.nth_le_zip {α : Type u} {β : Type v} {l : list α} {l' : list β} {i : } {h : i < (l.zip l').length} :
(l.zip l').nth_le i h = (l.nth_le i _, l'.nth_le i _)
theorem list.mem_zip_inits_tails {α : Type u} {l init tail : list α} :
(init, tail) l.inits.zip l.tails init ++ tail = l
theorem list.map_uncurry_zip_eq_zip_with {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : list α) (l' : list β) :
@[simp]
theorem list.sum_zip_with_distrib_left {α : Type u} {β : Type v} {γ : Type u_1} [semiring γ] (f : α → β → γ) (n : γ) (l : list α) (l' : list β) :
(list.zip_with (λ (x : α) (y : β), n * f x y) l l').sum = n * (list.zip_with f l l').sum