Documentation

Mathlib.Init.Data.List.Lemmas

Lemmas for List not (yet) in Std

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_bex_nil {α : Type u} (p : αProp) :
¬∃ (x : α), x [] p x
theorem List.bex_cons {α : Type u} (p : αProp) (a : α) (l : List α) :
(∃ (x : α), x a :: l p x) p a ∃ (x : α), x l p x

list subset

sublists

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

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

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

      Length of a list obtained using mapAccumr₂.