mathlib docs: data.list.zip

source

@[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₂

source

@[simp]

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

list.nil.zip l = list.nil

source

@[simp]

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

l.zip list.nil = list.nil

source

@[simp]

theorem list.zip_swap {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :

list.map prod.swap (l₁.zip l₂) = l₂.zip l₁

source

@[simp]

theorem list.length_zip {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :

(l₁.zip l₂).length = min l₁.length l₂.length

source

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₂

source

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₂)

source

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₂)

source

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₂)

source

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

source

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

(a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂

source

theorem list.map_fst_zip {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :

l₁.length ≤ l₂.length → list.map prod.fst (l₁.zip l₂) = l₁

source

theorem list.map_snd_zip {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :

l₂.length ≤ l₁.length → list.map prod.snd (l₁.zip l₂) = l₂

source

@[simp]

theorem list.unzip_nil {α : Type u} {β : Type v} :

list.nil.unzip = (list.nil α, list.nil β)

source

@[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)

source

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

l.unzip = (list.map prod.fst l, list.map prod.snd l)

source

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

l.unzip.fst = list.map prod.fst l

source

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

l.unzip.snd = list.map prod.snd l

source

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

(list.map prod.swap l).unzip = l.unzip.swap

source

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

l.unzip.fst.zip l.unzip.snd = l

source

theorem list.unzip_zip_left {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} :

l₁.length ≤ l₂.length → (l₁.zip l₂).unzip.fst = l₁

source

theorem list.unzip_zip_right {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} :

l₂.length ≤ l₁.length → (l₁.zip l₂).unzip.snd = l₂

source

theorem list.unzip_zip {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} :

l₁.length = l₂.length → (l₁.zip l₂).unzip = (l₁, l₂)

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 α) :

list.map prod.fst l.revzip = l

source

@[simp]

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

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 α) :

list.map prod.swap l.revzip = l.reverse.revzip

mathlib documentation

data.list.zip

General documentation

Additional documentation

Library

mathlib documentation

data.​list.​zip

General documentation

Additional documentation

Library

data.list.zip