mathlib docs: 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

@[simp]

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

@[simp]

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

a ∈ l₁ → a ∈ l₁ ++ l₂

source

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

a ∈ l₂ → a ∈ l₁ ++ l₂

source

@[simp]

theorem list.not_bex_nil {α : Type u} (p : α → Prop) :

¬∃ (x : α) (H : x ∈ list.nil), p x

source

@[simp]

theorem list.ball_nil {α : Type u} (p : α → Prop) (x : α) :

x ∈ list.nil → p x

source

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

source

@[simp]

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

def list.subset {α : Type u} :

list α → list α → Prop

Equations

l₁.subset l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂

source

@[instance]

def list.has_subset {α : Type u} :

has_subset (list α)

Equations

list.has_subset = {subset := list.subset α}

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

l₁ ⊆ l₂ → 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 : α) :

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₂} :

(α → σ → σ × β) → list α → σ → σ × list β

Equations

list.map_accumr f (y :: yr) c = let r : σ × list β := list.map_accumr f yr c, z : σ × β := f y r.fst in (z.fst, z.snd :: r.snd)
list.map_accumr f list.nil c = (c, list.nil β)

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₂} :

(α → β → σ → σ × φ) → list α → list β → σ → σ × list φ

Equations

list.map_accumr₂ f (x :: xr) (y :: yr) c = let r : σ × list φ := list.map_accumr₂ f xr yr c, q : σ × φ := f x y r.fst in (q.fst, q.snd :: r.snd)
list.map_accumr₂ f (hd :: tl) list.nil c = (c, list.nil φ)
list.map_accumr₂ f list.nil (hd :: tl) c = (c, list.nil φ)
list.map_accumr₂ f list.nil list.nil c = (c, list.nil φ)

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

mathlib documentation

core.init.data.list.lemmas

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​data.​list.​lemmas

General documentation

Additional documentation

Library

core.init.data.list.lemmas