mathlib3 documentation

core / init.data.list.lemmas

append

@[simp]
theorem list.nil_append {α : Type u} (s : list α) :
@[simp]
theorem list.cons_append {α : Type u} (x : α) (s t : list α) :
x :: s ++ t = x :: (s ++ t)
@[simp]
theorem list.append_nil {α : Type u} (t : list α) :
@[simp]
theorem list.append_assoc {α : Type u} (s t u : list α) :
s ++ t ++ u = s ++ (t ++ u)

length

theorem list.length_cons {α : Type u} (a : α) (l : list α) :
(a :: l).length = l.length + 1
@[simp]
theorem list.length_append {α : Type u} (s t : list α) :
(s ++ t).length = s.length + t.length
@[simp]
theorem list.length_repeat {α : Type u} (a : α) (n : ) :
@[simp]
theorem list.length_tail {α : Type u} (l : list α) :
@[simp]
theorem list.length_drop {α : Type u} (i : ) (l : list α) :

map

theorem list.map_cons {α : Type u} {β : Type v} (f : α β) (a : α) (l : list α) :
list.map f (a :: l) = f a :: list.map f l
@[simp]
theorem list.map_append {α : Type u} {β : Type v} (f : α β) (l₁ l₂ : list α) :
list.map f (l₁ ++ l₂) = list.map f l₁ ++ list.map f l₂
theorem list.map_singleton {α : Type u} {β : Type v} (f : α β) (a : α) :
list.map f [a] = [f a]
@[simp]
theorem list.map_id {α : Type u} (l : list α) :
@[simp]
theorem list.map_map {α : Type u} {β : Type v} {γ : Type w} (g : β γ) (f : α β) (l : list α) :
list.map g (list.map f l) = list.map (g f) l
@[simp]
theorem list.length_map {α : Type u} {β : Type v} (f : α β) (l : list α) :

bind

@[simp]
theorem list.nil_bind {α : Type u} {β : Type v} (f : α list β) :
@[simp]
theorem list.cons_bind {α : Type u} {β : Type v} (x : α) (xs : list α) (f : α list β) :
(x :: xs).bind f = f x ++ xs.bind f
@[simp]
theorem list.append_bind {α : Type u} {β : Type v} (xs ys : list α) (f : α list β) :
(xs ++ ys).bind f = xs.bind f ++ ys.bind f

mem

theorem list.mem_nil_iff {α : Type u} (a : α) :
@[simp]
theorem list.not_mem_nil {α : Type u} (a : α) :
theorem list.mem_cons_self {α : Type u} (a : α) (l : list α) :
a a :: l
@[simp]
theorem list.mem_cons_iff {α : Type u} (a y : α) (l : list α) :
a y :: l a = y a l
theorem list.mem_cons_eq {α : Type u} (a y : α) (l : list α) :
a y :: l = (a = y a l)
theorem list.mem_cons_of_mem {α : Type u} (y : α) {a : α} {l : list α} :
a l a y :: l
theorem list.eq_or_mem_of_mem_cons {α : Type u} {a y : α} {l : list α} :
a y :: l a = y a l
@[simp]
theorem list.mem_append {α : Type u} {a : α} {s t : list α} :
a s ++ t a s a t
theorem list.mem_append_eq {α : Type u} (a : α) (s t : list α) :
a s ++ t = (a s a t)
theorem list.mem_append_left {α : Type u} {a : α} {l₁ : list α} (l₂ : list α) (h : a l₁) :
a l₁ ++ l₂
theorem list.mem_append_right {α : Type u} {a : α} (l₁ : list α) {l₂ : list α} (h : a l₂) :
a l₁ ++ l₂
theorem list.not_bex_nil {α : Type u} (p : α Prop) :
¬ (x : α) (H : x list.nil), p x
theorem list.ball_nil {α : Type u} (p : α Prop) (x : α) (H : x list.nil) :
p x
theorem list.bex_cons {α : Type u} (p : α Prop) (a : α) (l : list α) :
( (x : α) (H : x a :: l), p x) p a (x : α) (H : x l), p x
theorem list.ball_cons {α : Type u} (p : α Prop) (a : α) (l : list α) :
( (x : α), x a :: l p x) p a (x : α), x l p x

list subset

@[protected]
def list.subset {α : Type u} (l₁ l₂ : list α) :
Prop
Equations
@[protected, instance]
def list.has_subset {α : Type u} :
Equations
@[simp]
theorem list.nil_subset {α : Type u} (l : list α) :
@[simp, refl]
theorem list.subset.refl {α : Type u} (l : list α) :
l l
@[trans]
theorem list.subset.trans {α : Type u} {l₁ l₂ l₃ : list α} (h₁ : l₁ l₂) (h₂ : l₂ l₃) :
l₁ l₃
@[simp]
theorem list.subset_cons {α : Type u} (a : α) (l : list α) :
l a :: l
theorem list.subset_of_cons_subset {α : Type u} {a : α} {l₁ l₂ : list α} :
a :: l₁ l₂ l₁ l₂
theorem list.cons_subset_cons {α : Type u} {l₁ l₂ : list α} (a : α) (s : l₁ l₂) :
a :: l₁ a :: l₂
@[simp]
theorem list.subset_append_left {α : Type u} (l₁ l₂ : list α) :
l₁ l₁ ++ l₂
@[simp]
theorem list.subset_append_right {α : Type u} (l₁ l₂ : list α) :
l₂ l₁ ++ l₂
theorem list.subset_cons_of_subset {α : Type u} (a : α) {l₁ l₂ : list α} :
l₁ l₂ l₁ a :: l₂
theorem list.eq_nil_of_length_eq_zero {α : Type u} {l : list α} :
theorem list.ne_nil_of_length_eq_succ {α : Type u} {l : list α} {n : } :
@[simp]
theorem list.length_map₂ {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) (l₁ : list α) (l₂ : list β) :
@[simp]
theorem list.length_take {α : Type u} (i : ) (l : list α) :
theorem list.length_take_le {α : Type u} (n : ) (l : list α) :
theorem list.length_remove_nth {α : Type u} (l : list α) (i : ) :
@[simp]
theorem list.partition_eq_filter_filter {α : Type u} (p : α Prop) [decidable_pred p] (l : list α) :

sublists

inductive list.sublist {α : Type u} :
list α list α Prop
Instances for list.sublist
theorem list.length_le_of_sublist {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂ l₁.length l₂.length

filter

@[simp]
theorem list.filter_nil {α : Type u} (p : α Prop) [h : decidable_pred p] :
@[simp]
theorem list.filter_cons_of_pos {α : Type u} {p : α Prop} [h : decidable_pred p] {a : α} (l : list α) :
p a list.filter p (a :: l) = a :: list.filter p l
@[simp]
theorem list.filter_cons_of_neg {α : Type u} {p : α Prop} [h : decidable_pred p] {a : α} (l : list α) :
¬p a list.filter p (a :: l) = list.filter p l
@[simp]
theorem list.filter_append {α : Type u} {p : α Prop} [h : decidable_pred p] (l₁ l₂ : list α) :
list.filter p (l₁ ++ l₂) = list.filter p l₁ ++ list.filter p l₂
@[simp]
theorem list.filter_sublist {α : Type u} {p : α Prop} [h : decidable_pred p] (l : list α) :

map_accumr

def list.map_accumr {α : Type u} {β : Type v} {σ : Type w₂} (f : α σ σ × β) :
list α σ σ × list β
Equations
@[simp]
theorem list.length_map_accumr {α : Type u} {β : Type v} {σ : Type w₂} (f : α σ σ × β) (x : list α) (s : σ) :
def list.map_accumr₂ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : α β σ σ × φ) :
list α list β σ σ × list φ
Equations
@[simp]
theorem list.length_map_accumr₂ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : α β σ σ × φ) (x : list α) (y : list β) (c : σ) :