Documentation

Mathlib.Init.Data.List.Lemmas

Lemmas for List not (yet) in Batteries

append

length

map

bind

mem

theorem List.mem_cons_eq {α : Type u} (a : α) (y : α) (l : List α) :
(a y :: l) = (a = y a l)
theorem List.eq_or_mem_of_mem_cons :
∀ {α : Type u_1} {a b : α} {l : List α}, a b :: la = b a l

Alias of the forward direction of List.mem_cons.

theorem List.not_exists_mem_nil {α : Type u} (p : αProp) :
¬∃ (x : α), x [] p x
@[deprecated List.not_exists_mem_nil]
theorem List.not_bex_nil {α : Type u} (p : αProp) :
¬∃ (x : α), x [] p x

Alias of List.not_exists_mem_nil.

@[deprecated List.exists_mem_cons]
theorem List.bex_cons {α : Type u_1} {p : αProp} {a : α} {l : List α} :
(∃ (x : α), ∃ (x_1 : x a :: l), p x) p a ∃ (x : α), ∃ (x_1 : x l), p x

Alias of List.exists_mem_cons.

list subset

sublists

theorem List.length_le_of_sublist :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₁.length l₂.length

Alias of List.Sublist.length_le.

filter

map_accumr

def List.mapAccumr {α : Type u} {β : Type v} {σ : Type w₂} (f : ασσ × β) :
List ασσ × List β

Runs a function over a list returning the intermediate results and a final result.

Equations
Instances For
    @[simp]
    theorem List.length_mapAccumr {α : Type u} {β : Type v} {σ : Type w₂} (f : ασσ × β) (x : List α) (s : σ) :
    (List.mapAccumr f x s).snd.length = x.length

    Length of the list obtained by mapAccumr.

    def List.mapAccumr₂ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : αβσσ × φ) :
    List αList βσσ × List φ

    Runs a function over two lists returning the intermediate results and a final result.

    Equations
    Instances For
      @[simp]
      theorem List.length_mapAccumr₂ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : αβσσ × φ) (x : List α) (y : List β) (c : σ) :
      (List.mapAccumr₂ f x y c).snd.length = min x.length y.length

      Length of a list obtained using mapAccumr₂.