mathlib documentation

core.init.data.list.lemmas

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

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

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

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

@[simp]
theorem list.mem_nil_iff {α : Type u} (a : α) :

@[simp]
theorem list.not_mem_nil {α : Type u} (a : α) :

@[simp]
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 la y :: l

theorem list.eq_or_mem_of_mem_cons {α : Type u} {a y : α} {l : list α} :
a y :: la = 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 α) :
a l₁a l₁ ++ l₂

theorem list.mem_append_right {α : Type u} {a : α} (l₁ : list α) {l₂ : list α} :
a l₂a l₁ ++ l₂

@[simp]
theorem list.not_bex_nil {α : Type u} (p : α → Prop) :
¬∃ (x : α) (H : x list.nil), p x

@[simp]
theorem list.ball_nil {α : Type u} (p : α → Prop) (x : α) :
x list.nilp x

@[simp]
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

@[simp]
theorem list.ball_cons {α : Type u} (p : α → Prop) (a : α) (l : list α) :
(∀ (x : α), x a :: lp x) p a ∀ (x : α), x lp x

def list.subset {α : Type u} :
list αlist α → Prop

Equations
@[instance]
def list.has_subset {α : Type u} :

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

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

theorem list.subset.trans {α : Type u} {l₁ l₂ l₃ : list α} :
l₁ l₂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 : α) :
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 α} :
l.length = 0l = list.nil

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 β) :
(list.map₂ f l₁ l₂).length = min l₁.length l₂.length

@[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 : ) :
i < l.length(l.remove_nth i).length = l.length - 1

@[simp]
theorem list.partition_eq_filter_filter {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :

inductive list.sublist {α : Type u} :
list αlist α → Prop
  • slnil : ∀ {α : Type u}, list.nil <+ list.nil
  • cons : ∀ {α : Type u} (l₁ l₂ : list α) (a : α), l₁ <+ l₂l₁ <+ a :: l₂
  • cons2 : ∀ {α : Type u} (l₁ l₂ : list α) (a : α), l₁ <+ l₂a :: l₁ <+ a :: l₂

theorem list.length_le_of_sublist {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂l₁.length l₂.length

@[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 alist.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 alist.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 α) :

def list.map_accumr {α : Type u} {β : Type v} {σ : Type w₂} :
(α → σ → σ × β)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₂} :
(α → β → σ → σ × φ)list αlist βσ → σ × list φ

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