mathlib documentation

core / init.data.list.lemmas

source
@[simp]
theorem list.nil_append {α : Type u} (s : list α) :
list.nil ++ s = s
source
@[simp]
theorem list.cons_append {α : Type u} (x : α) (s t : list α) :
x :: s ++ t = x :: (s ++ t)
source
@[simp]
theorem list.append_nil {α : Type u} (t : list α) :
t ++ list.nil = t
source
@[simp]
theorem list.append_assoc {α : Type u} (s t u : list α) :
s ++ t ++ u = s ++ (t ++ u)
source
theorem list.length_cons {α : Type u} (a : α) (l : list α) :
(a :: l).length = l.length + 1
source
@[simp]
theorem list.length_append {α : Type u} (s t : list α) :
(s ++ t).length = s.length + t.length
source
@[simp]
theorem list.length_repeat {α : Type u} (a : α) (n : ℕ) :
(list.repeat a n).length = n
source
@[simp]
theorem list.length_tail {α : Type u} (l : list α) :
l.tail.length = l.length - 1
source
@[simp]
theorem list.length_drop {α : Type u} (i : ℕ) (l : list α) :
(list.drop i l).length = l.length - i
source
theorem list.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (l : list α) :
list.map f (a :: l) = f a :: list.map f l
source
@[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₂
source
theorem list.map_singleton {α : Type u} {β : Type v} (f : α → β) (a : α) :
list.map f [a] = [f a]
source
@[simp]
theorem list.map_id {α : Type u} (l : list α) :
list.map id l = l
source
@[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
source
@[simp]
theorem list.length_map {α : Type u} {β : Type v} (f : α → β) (l : list α) :
(list.map f l).length = l.length
source
@[simp]
theorem list.nil_bind {α : Type u} {β : Type v} (f : α → list β) :
list.nil.bind f = list.nil
source
@[simp]
theorem list.cons_bind {α : Type u} {β : Type v} (x : α) (xs : list α) (f : α → list β) :
(x :: xs).bind f = f x ++ xs.bind f
source
@[simp]
theorem list.append_bind {α : Type u} {β : Type v} (xs ys : list α) (f : α → list β) :
(xs ++ ys).bind f = xs.bind f ++ ys.bind f
source
theorem list.mem_nil_iff {α : Type u} (a : α) :
a ∈ list.nil ↔ false
source
@[simp]
theorem list.not_mem_nil {α : Type u} (a : α) :
a ∉ list.nil
source
theorem list.mem_cons_self {α : Type u} (a : α) (l : list α) :
a ∈ a :: l
source
@[simp]
theorem list.mem_cons_iff {α : Type u} (a y : α) (l : list α) :
a ∈ y :: l ↔ a = y ∨ a ∈ l
source
theorem list.mem_cons_eq {α : Type u} (a y : α) (l : list α) :
a ∈ y :: l = (a = y ∨ a ∈ l)
source
theorem list.mem_cons_of_mem {α : Type u} (y : α) {a : α} {l : list α} :
a ∈ l → a ∈ y :: l
source
theorem list.eq_or_mem_of_mem_cons {α : Type u} {a y : α} {l : list α} :
a ∈ y :: l → a = y ∨ a ∈ l
source
@[simp]
theorem list.mem_append {α : Type u} {a : α} {s t : list α} :
a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t
source
theorem list.mem_append_eq {α : Type u} (a : α) (s t : list α) :
a ∈ s ++ t = (a ∈ s ∨ a ∈ t)
source
theorem list.mem_append_left {α : Type u} {a : α} {l₁ : list α} (l₂ : list α) (h : a ∈ l₁) :
a ∈ l₁ ++ l₂
source
theorem list.mem_append_right {α : Type u} {a : α} (l₁ : list α) {l₂ : list α} (h : a ∈ l₂) :
a ∈ l₁ ++ l₂
source
theorem list.not_bex_nil {α : Type u} (p : α → Prop) :
¬∃ (x : α) (H : x ∈ list.nil), p x
source
theorem list.ball_nil {α : Type u} (p : α → Prop) (x : α) (H : x ∈ list.nil) :
p x
source
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
source
theorem list.ball_cons {α : Type u} (p : α → Prop) (a : α) (l : list α) :
(∀ (x : α), x ∈ a :: l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l → p x
source
@[protected]
def list.subset {α : Type u} (l₁ l₂ : list α) :
Prop
Equations
source
@[protected, instance]
def list.has_subset {α : Type u} :
has_subset (list α)
Equations
source
@[simp]
theorem list.nil_subset {α : Type u} (l : list α) :
list.nil ⊆ l
source
@[simp]
theorem list.subset.refl {α : Type u} (l : list α) :
l ⊆ l
source
theorem list.subset.trans {α : Type u} {l₁ l₂ l₃ : list α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) :
l₁ ⊆ l₃
source
@[simp]
theorem list.subset_cons {α : Type u} (a : α) (l : list α) :
l ⊆ a :: l
source
theorem list.subset_of_cons_subset {α : Type u} {a : α} {l₁ l₂ : list α} :
a :: l₁ ⊆ l₂ → l₁ ⊆ l₂
source
theorem list.cons_subset_cons {α : Type u} {l₁ l₂ : list α} (a : α) (s : l₁ ⊆ l₂) :
a :: l₁ ⊆ a :: l₂
source
@[simp]
theorem list.subset_append_left {α : Type u} (l₁ l₂ : list α) :
l₁ ⊆ l₁ ++ l₂
source
@[simp]
theorem list.subset_append_right {α : Type u} (l₁ l₂ : list α) :
l₂ ⊆ l₁ ++ l₂
source
theorem list.subset_cons_of_subset {α : Type u} (a : α) {l₁ l₂ : list α} :
l₁ ⊆ l₂ → l₁ ⊆ a :: l₂
source
theorem list.eq_nil_of_length_eq_zero {α : Type u} {l : list α} :
l.length = 0 → l = list.nil
source
theorem list.ne_nil_of_length_eq_succ {α : Type u} {l : list α} {n : ℕ} :
l.length = n.succ → l ≠ list.nil
source
@[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
source
@[simp]
theorem list.length_take {α : Type u} (i : ℕ) (l : list α) :
(list.take i l).length = min i l.length
source
theorem list.length_take_le {α : Type u} (n : ℕ) (l : list α) :
(list.take n l).length ≤ n
source
theorem list.length_remove_nth {α : Type u} (l : list α) (i : ℕ) :
i < l.length → (l.remove_nth i).length = l.length - 1
source
@[simp]
theorem list.partition_eq_filter_filter {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
list.partition p l = (list.filter p l, list.filter (not ∘ p) l)
source
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₂
source
theorem list.length_le_of_sublist {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂ → l₁.length ≤ l₂.length
source
@[simp]
theorem list.filter_nil {α : Type u} (p : α → Prop) [h : decidable_pred p] :
list.filter p list.nil = list.nil
source
@[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
source
@[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
source
@[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₂
source
@[simp]
theorem list.filter_sublist {α : Type u} {p : α → Prop} [h : decidable_pred p] (l : list α) :
list.filter p l <+ l
source
def list.map_accumr {α : Type u} {β : Type v} {σ : Type w₂} (f : α → σ → σ × β) :
list α → σ → σ × list β
Equations
source
@[simp]
theorem list.length_map_accumr {α : Type u} {β : Type v} {σ : Type w₂} (f : α → σ → σ × β) (x : list α) (s : σ) :
(list.map_accumr f x s).snd.length = x.length
source
def list.map_accumr₂ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : α → β → σ → σ × φ) :
list α → list β → σ → σ × list φ
Equations
source
@[simp]
theorem list.length_map_accumr₂ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : α → β → σ → σ × φ) (x : list α) (y : list β) (c : σ) :
(list.map_accumr₂ f x y c).snd.length = min x.length y.length