# Basic properties of lists #

source
instance List.uniqueOfIsEmpty {α : Type u} [IsEmpty α] :
Unique (List α)

There is only one list of an empty type

Equations

- List.uniqueOfIsEmpty = { toInhabited := instInhabitedList, uniq := ⋯ }

source
instance List.instLawfulIdentityAppendNil_mathlib {α : Type u} :
Std.LawfulIdentity Append.append []
source
instance List.instAssociativeAppend_mathlib {α : Type u} :
Std.Associative Append.append
source
@[simp]
theorem List.cons_injective {α : Type u} {a : α} :
Function.Injective (cons a)
source
theorem List.singleton_injective {α : Type u} :
Function.Injective fun (a : α) => [a]
source
theorem List.set_of_mem_cons {α : Type u} (l : List α) (a : α) :
{x : α | x ∈ a :: l} = insert a {x : α | x ∈ l}

### mem #

source
theorem Decidable.List.eq_or_ne_mem_of_mem {α : Type u} [DecidableEq α] {a b : α} {l : List α} (h : a ∈ b :: l) :
a = b ∨ a ≠ b ∧ a ∈ l
source
theorem List.mem_pair {α : Type u} {a b c : α} :
a ∈ [b, c] ↔ a = b ∨ a = c
source
@[simp]
theorem List.mem_map_of_injective {α : Type u} {β : Type v} {f : α → β} (H : Function.Injective f) {a : α} {l : List α} :
f a ∈ map f l ↔ a ∈ l
source
@[simp]
theorem Function.Involutive.exists_mem_and_apply_eq_iff {α : Type u} {f : α → α} (hf : Involutive f) (x : α) (l : List α) :
(∃ (y : α), y ∈ l ∧ f y = x) ↔ f x ∈ l
source
theorem List.mem_map_of_involutive {α : Type u} {f : α → α} (hf : Function.Involutive f) {a : α} {l : List α} :
a ∈ map f l ↔ f a ∈ l

### length #

source
theorem List.length_pos_of_ne_nil {α : Type u_1} {l : List α} :
l ≠ [] → 0 < l.length

Alias of the reverse direction of `List.length_pos_iff`.

source
theorem List.length_pos_iff_ne_nil {α : Type u} {l : List α} :
0 < l.length ↔ l ≠ []
source
theorem List.exists_of_length_succ {α : Type u} {n : ℕ} (l : List α) :
l.length = n + 1 → ∃ (h : α), ∃ (t : List α), l = h :: t
source
@[simp]
theorem List.length_injective_iff {α : Type u} :
Function.Injective length ↔ Subsingleton α
source
@[simp]
theorem List.length_injective {α : Type u} [Subsingleton α] :
Function.Injective length
source
theorem List.length_eq_two {α : Type u} {l : List α} :
l.length = 2 ↔ ∃ (a : α), ∃ (b : α), l = [a, b]
source
theorem List.length_eq_three {α : Type u} {l : List α} :
l.length = 3 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), l = [a, b, c]
source
theorem List.length_eq_four {α : Type u} {l : List α} :
l.length = 4 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), ∃ (d : α), l = [a, b, c, d]

### set-theoretic notation of lists #

source
instance List.instSingletonList {α : Type u} :
Singleton α (List α)
Equations

- List.instSingletonList = { singleton := fun (x : α) => [x] }

source
instance List.instInsertOfDecidableEq_mathlib {α : Type u} [DecidableEq α] :
Insert α (List α)
Equations

- List.instInsertOfDecidableEq_mathlib = { insert := List.insert }

source
instance List.instLawfulSingleton_mathlib {α : Type u} [DecidableEq α] :
LawfulSingleton α (List α)
source
theorem List.singleton_eq {α : Type u} (x : α) :
{x} = [x]
source
theorem List.insert_neg {α : Type u} [DecidableEq α] {x : α} {l : List α} (h : ¬x ∈ l) :
insert x l = x :: l
source
theorem List.insert_pos {α : Type u} [DecidableEq α] {x : α} {l : List α} (h : x ∈ l) :
insert x l = l
source
theorem List.doubleton_eq {α : Type u} [DecidableEq α] {x y : α} (h : x ≠ y) :
{x, y} = [x, y]

### bounded quantifiers over lists #

source
theorem List.forall_mem_of_forall_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : List α} (h : ∀ (x : α), x ∈ a :: l → p x) (x : α) :
x ∈ l → p x
source
theorem List.exists_mem_cons_of {α : Type u} {p : α → Prop} {a : α} (l : List α) (h : p a) :
∃ (x : α), x ∈ a :: l ∧ p x
source
theorem List.exists_mem_cons_of_exists {α : Type u} {p : α → Prop} {a : α} {l : List α} :
(∃ (x : α), x ∈ l ∧ p x) → ∃ (x : α), x ∈ a :: l ∧ p x
source
theorem List.or_exists_of_exists_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : List α} :
(∃ (x : α), x ∈ a :: l ∧ p x) → p a ∨ ∃ (x : α), x ∈ l ∧ p x
source
theorem List.exists_mem_cons_iff {α : Type u} (p : α → Prop) (a : α) (l : List α) :
(∃ (x : α), x ∈ a :: l ∧ p x) ↔ p a ∨ ∃ (x : α), x ∈ l ∧ p x

### list subset #

source
theorem List.cons_subset_of_subset_of_mem {α : Type u} {a : α} {l m : List α} (ainm : a ∈ m) (lsubm : l ⊆ m) :
a :: l ⊆ m
source
theorem List.append_subset_of_subset_of_subset {α : Type u} {l₁ l₂ l : List α} (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) :
l₁ ++ l₂ ⊆ l
source
theorem List.map_subset_iff {α : Type u} {β : Type v} {l₁ l₂ : List α} (f : α → β) (h : Function.Injective f) :
map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

### append #

source
theorem List.append_eq_has_append {α : Type u} {L₁ L₂ : List α} :
L₁.append L₂ = L₁ ++ L₂
source
theorem List.append_right_injective {α : Type u} (s : List α) :
Function.Injective fun (t : List α) => s ++ t
source
theorem List.append_left_injective {α : Type u} (t : List α) :
Function.Injective fun (s : List α) => s ++ t

### replicate #

source
theorem List.eq_replicate_length {α : Type u} {a : α} {l : List α} :
l = replicate l.length a ↔ ∀ (b : α), b ∈ l → b = a
source
theorem List.replicate_add {α : Type u} (m n : ℕ) (a : α) :
replicate (m + n) a = replicate m a ++ replicate n a
source
theorem List.replicate_subset_singleton {α : Type u} (n : ℕ) (a : α) :
replicate n a ⊆ [a]
source
theorem List.subset_singleton_iff {α : Type u} {a : α} {L : List α} :
L ⊆ [a] ↔ ∃ (n : ℕ), L = replicate n a
source
theorem List.replicate_right_injective {α : Type u} {n : ℕ} (hn : n ≠ 0) :
Function.Injective (replicate n)
source
theorem List.replicate_right_inj {α : Type u} {a b : α} {n : ℕ} (hn : n ≠ 0) :
replicate n a = replicate n b ↔ a = b
source
theorem List.replicate_right_inj' {α : Type u} {a b : α} {n : ℕ} :
replicate n a = replicate n b ↔ n = 0 ∨ a = b
source
theorem List.replicate_left_injective {α : Type u} (a : α) :
Function.Injective fun (x : ℕ) => replicate x a
source
theorem List.replicate_left_inj {α : Type u} {a : α} {n m : ℕ} :
replicate n a = replicate m a ↔ n = m
source
@[simp]
theorem List.head?_flatten_replicate {α : Type u} {n : ℕ} (h : n ≠ 0) (l : List α) :
(replicate n l).flatten.head? = l.head?
source
@[simp]
theorem List.getLast?_flatten_replicate {α : Type u} {n : ℕ} (h : n ≠ 0) (l : List α) :
(replicate n l).flatten.getLast? = l.getLast?

### pure #

source
theorem List.mem_pure {α : Type u} (x y : α) :
x ∈ pure y ↔ x = y

### bind #

source
@[simp]
theorem List.bind_eq_flatMap {α β : Type u_2} (f : α → List β) (l : List α) :
l >>= f = flatMap f l

### concat #

### reverse #

source
theorem List.reverse_cons' {α : Type u} (a : α) (l : List α) :
(a :: l).reverse = l.reverse.concat a
source
theorem List.reverse_concat' {α : Type u} (l : List α) (a : α) :
(l ++ [a]).reverse = a :: l.reverse
source
@[simp]
theorem List.reverse_singleton {α : Type u} (a : α) :
[a].reverse = [a]
source
@[simp]
theorem List.reverse_involutive {α : Type u} :
Function.Involutive reverse
source
@[simp]
theorem List.reverse_injective {α : Type u} :
Function.Injective reverse
source
theorem List.reverse_surjective {α : Type u} :
Function.Surjective reverse
source
theorem List.reverse_bijective {α : Type u} :
Function.Bijective reverse
source
theorem List.concat_eq_reverse_cons {α : Type u} (a : α) (l : List α) :
l.concat a = (a :: l.reverse).reverse
source
theorem List.map_reverseAux {α : Type u} {β : Type v} (f : α → β) (l₁ l₂ : List α) :
map f (l₁.reverseAux l₂) = (map f l₁).reverseAux (map f l₂)
source
@[simp]
theorem List.reverse_perm' {α : Type u} {l₁ l₂ : List α} :
l₁.reverse.Perm l₂ ↔ l₁.Perm l₂
source
@[simp]
theorem List.perm_reverse {α : Type u} {l₁ l₂ : List α} :
l₁.Perm l₂.reverse ↔ l₁.Perm l₂

### getLast #

source
theorem List.getLast_append_singleton {α : Type u} {a : α} (l : List α) :
(l ++ [a]).getLast ⋯ = a
source
theorem List.getLast_append_of_right_ne_nil {α : Type u} (l₁ l₂ : List α) (h : l₂ ≠ []) :
(l₁ ++ l₂).getLast ⋯ = l₂.getLast h
source
theorem List.getLast_concat' {α : Type u} {a : α} (l : List α) :
(l.concat a).getLast ⋯ = a
source
@[simp]
theorem List.getLast_singleton' {α : Type u} (a : α) :
[a].getLast ⋯ = a
source
theorem List.dropLast_append_getLast {α : Type u} {l : List α} (h : l ≠ []) :
l.dropLast ++ [l.getLast h] = l
source
theorem List.getLast_congr {α : Type u} {l₁ l₂ : List α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) :
l₁.getLast h₁ = l₂.getLast h₂
source
theorem List.getLast_replicate_succ {α : Type u} (m : ℕ) (a : α) :
(replicate (m + 1) a).getLast ⋯ = a

### getLast? #

source
theorem List.mem_getLast?_eq_getLast {α : Type u} {l : List α} {x : α} :
x ∈ l.getLast? → ∃ (h : l ≠ []), x = l.getLast h
source
theorem List.getLast?_eq_getLast_of_ne_nil {α : Type u} {l : List α} (h : l ≠ []) :
l.getLast? = some (l.getLast h)
source
theorem List.mem_getLast?_cons {α : Type u} {x y : α} {l : List α} :
x ∈ l.getLast? → x ∈ (y :: l).getLast?
source
theorem List.dropLast_append_getLast? {α : Type u} {l : List α} (a : α) :
a ∈ l.getLast? → l.dropLast ++ [a] = l
source
theorem List.getLastI_eq_getLast? {α : Type u} [Inhabited α] (l : List α) :
l.getLastI = l.getLast?.iget
source
theorem List.getLast?_append_cons {α : Type u} (l₁ : List α) (a : α) (l₂ : List α) :
(l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
source
theorem List.getLast?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} :
l₂ ≠ [] → (l₁ ++ l₂).getLast? = l₂.getLast?
source
theorem List.mem_getLast?_append_of_mem_getLast? {α : Type u} {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?) :
x ∈ (l₁ ++ l₂).getLast?

### head(!?) and tail #

source
@[simp]
theorem List.head!_nil {α : Type u} [Inhabited α] :
[].head! = default
source
@[deprecated List.cons_head_tail (since := "2025-08-15")]
theorem List.head_cons_tail {α : Type u} (x : List α) (h : x ≠ []) :
x.head h :: x.tail = x
source
theorem List.head_eq_getElem_zero {α : Type u} {l : List α} (hl : l ≠ []) :
l.head hl = l[0]
source
theorem List.head!_eq_head? {α : Type u} [Inhabited α] (l : List α) :
l.head! = l.head?.iget
source
theorem List.surjective_head! {α : Type u} [Inhabited α] :
Function.Surjective head!
source
theorem List.surjective_head? {α : Type u} :
Function.Surjective head?
source
theorem List.surjective_tail {α : Type u} :
Function.Surjective tail
source
theorem List.eq_cons_of_mem_head? {α : Type u} {x : α} {l : List α} :
x ∈ l.head? → l = x :: l.tail
source
@[simp]
theorem List.head!_cons {α : Type u} [Inhabited α] (a : α) (l : List α) :
(a :: l).head! = a
source
@[simp]
theorem List.head!_append {α : Type u} [Inhabited α] (t : List α) {s : List α} (h : s ≠ []) :
(s ++ t).head! = s.head!
source
theorem List.mem_head?_append_of_mem_head? {α : Type u} {s t : List α} {x : α} (h : x ∈ s.head?) :
x ∈ (s ++ t).head?
source
theorem List.head?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} :
l₁ ≠ [] → (l₁ ++ l₂).head? = l₁.head?
source
theorem List.tail_append_singleton_of_ne_nil {α : Type u} {a : α} {l : List α} (h : l ≠ []) :
(l ++ [a]).tail = l.tail ++ [a]
source
theorem List.cons_head?_tail {α : Type u} {l : List α} {a : α} :
a ∈ l.head? → a :: l.tail = l
source
theorem List.head!_mem_head? {α : Type u} [Inhabited α] {l : List α} :
l ≠ [] → l.head! ∈ l.head?
source
theorem List.cons_head!_tail {α : Type u} [Inhabited α] {l : List α} (h : l ≠ []) :
l.head! :: l.tail = l
source
theorem List.head!_mem_self {α : Type u} [Inhabited α] {l : List α} (h : l ≠ []) :
l.head! ∈ l
source
theorem List.get_eq_getElem? {α : Type u} (l : List α) (i : Fin l.length) :
l.get i = l[i]?.get ⋯
source
theorem List.exists_mem_iff_getElem {α : Type u} {l : List α} {p : α → Prop} :
(∃ (x : α), x ∈ l ∧ p x) ↔ ∃ (i : ℕ), ∃ (x : i < l.length), p l[i]
source
theorem List.forall_mem_iff_getElem {α : Type u} {l : List α} {p : α → Prop} :
(∀ (x : α), x ∈ l → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p l[i]
source
@[simp]
theorem List.get_surjective_iff {α : Type u} {l : List α} :
Function.Surjective l.get ↔ ∀ (x : α), x ∈ l
source
@[simp]
theorem List.getElem_fin_surjective_iff {α : Type u} {l : List α} :
(Function.Surjective fun (n : Fin l.length) => l[↑n]) ↔ ∀ (x : α), x ∈ l
source
@[simp]
theorem List.getElem?_surjective_iff {α : Type u} {l : List α} :
(Function.Surjective fun (n : ℕ) => l[n]?) ↔ ∀ (x : α), x ∈ l
source
theorem List.get_tail {α : Type u} (l : List α) (i : ℕ) (h : i < l.tail.length) (h' : i + 1 < l.length := ⋯) :
l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩

### sublists #

source
theorem List.Sublist.cons_cons {α : Type u} {l₁ l₂ : List α} (a : α) (s : l₁.Sublist l₂) :
(a :: l₁).Sublist (a :: l₂)
source
theorem List.cons_sublist_cons' {α : Type u} {l₁ l₂ : List α} {a b : α} :
(a :: l₁).Sublist (b :: l₂) ↔ (a :: l₁).Sublist l₂ ∨ a = b ∧ l₁.Sublist l₂
source
theorem List.sublist_cons_of_sublist {α : Type u} {l₁ l₂ : List α} (a : α) (h : l₁.Sublist l₂) :
l₁.Sublist (a :: l₂)
source
@[simp]
theorem List.sublist_singleton {α : Type u} {l : List α} {a : α} :
l.Sublist [a] ↔ l = [] ∨ l = [a]
source
theorem List.Sublist.antisymm {α : Type u} {l₁ l₂ : List α} (s₁ : l₁.Sublist l₂) (s₂ : l₂.Sublist l₁) :
l₁ = l₂
source
theorem List.Sublist.of_cons_of_ne {α : Type u} {l₁ l₂ : List α} {a b : α} (h₁ : a ≠ b) (h₂ : (a :: l₁).Sublist (b :: l₂)) :
(a :: l₁).Sublist l₂

If the first element of two lists are different, then a sublist relation can be reduced.

### indexOf #

source
theorem List.idxOf_cons_eq {α : Type u} [DecidableEq α] {a b : α} (l : List α) :
b = a → idxOf a (b :: l) = 0
source
@[simp]
theorem List.idxOf_cons_ne {α : Type u} [DecidableEq α] {a b : α} (l : List α) :
b ≠ a → idxOf a (b :: l) = (idxOf a l).succ
source
theorem List.idxOf_eq_length_iff {α : Type u} [DecidableEq α] {a : α} {l : List α} :
idxOf a l = l.length ↔ ¬a ∈ l
source
@[simp]
theorem List.idxOf_of_notMem {α : Type u} [DecidableEq α] {l : List α} {a : α} :
¬a ∈ l → idxOf a l = l.length
source
@[deprecated List.idxOf_of_notMem (since := "2025-05-23")]
theorem List.idxOf_of_not_mem {α : Type u} [DecidableEq α] {l : List α} {a : α} :
¬a ∈ l → idxOf a l = l.length

Alias of `List.idxOf_of_notMem`.

source
theorem List.idxOf_append_of_mem {α : Type u} {l₁ l₂ : List α} [DecidableEq α] {a : α} (h : a ∈ l₁) :
idxOf a (l₁ ++ l₂) = idxOf a l₁
source
theorem List.idxOf_append_of_notMem {α : Type u} {l₁ l₂ : List α} [DecidableEq α] {a : α} (h : ¬a ∈ l₁) :
idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂
source
@[deprecated List.idxOf_append_of_notMem (since := "2025-05-23")]
theorem List.idxOf_append_of_not_mem {α : Type u} {l₁ l₂ : List α} [DecidableEq α] {a : α} (h : ¬a ∈ l₁) :
idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂

Alias of `List.idxOf_append_of_notMem`.

### nth element #

source
theorem List.getElem?_length {α : Type u} (l : List α) :
l[l.length]? = none
source
theorem List.getElem_map_rev {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : ℕ} {h : n < l.length} :
f l[n] = (map f l)[n]

A version of `getElem_map` that can be used for rewriting.

source
theorem List.get_length_sub_one {α : Type u} {l : List α} (h : l.length - 1 < l.length) :
l.get ⟨l.length - 1, h⟩ = l.getLast ⋯
source
theorem List.take_one_drop_eq_of_lt_length {α : Type u} {l : List α} {n : ℕ} (h : n < l.length) :
take 1 (drop n l) = [l.get ⟨n, h⟩]
source
theorem List.ext_getElem?' {α : Type u} {l₁ l₂ : List α} (h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?) :
l₁ = l₂
source
theorem List.ext_get_iff {α : Type u} {l₁ l₂ : List α} :
l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
source
theorem List.ext_getElem?_iff' {α : Type u} {l₁ l₂ : List α} :
l₁ = l₂ ↔ ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?
source
theorem List.ext_getElem! {α : Type u} {l₁ l₂ : List α} [Inhabited α] (hl : l₁.length = l₂.length) (h : ∀ (n : ℕ), l₁[n]! = l₂[n]!) :
l₁ = l₂

If two lists `l₁` and `l₂` are the same length and `l₁[n]! = l₂[n]!` for all `n`, then the lists are equal.

source
@[simp]
theorem List.getElem_idxOf {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : idxOf a l < l.length) :
l[idxOf a l] = a
source
theorem List.idxOf_get {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : idxOf a l < l.length) :
l.get ⟨idxOf a l, h⟩ = a
source
@[simp]
theorem List.getElem?_idxOf {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) :
l[idxOf a l]? = some a
source
theorem List.idxOf_inj {α : Type u} [DecidableEq α] {l : List α} {x y : α} (hx : x ∈ l) (hy : y ∈ l) :
idxOf x l = idxOf y l ↔ x = y
source
theorem List.get_reverse' {α : Type u} (l : List α) (n : Fin l.reverse.length) (hn' : l.length - 1 - ↑n < l.length) :
l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩
source
theorem List.eq_cons_of_length_one {α : Type u} {l : List α} (h : l.length = 1) :
l = [l.get ⟨0, ⋯⟩]
source
theorem List.getElem_set_of_ne {α : Type u} {l : List α} {i j : ℕ} (h : i ≠ j) (a : α) (hj : j < (l.set i a).length) :
(l.set i a)[j] = l[j]

### map #

source
theorem List.flatMap_pure_eq_map {α : Type u} {β : Type v} (f : α → β) (l : List α) :
flatMap (pure ∘ f) l = map f l
source
theorem List.flatMap_congr {α : Type u} {β : Type v} {l : List α} {f g : α → List β} (h : ∀ (x : α), x ∈ l → f x = g x) :
flatMap f l = flatMap g l
source
theorem List.infix_flatMap_of_mem {α : Type u} {a : α} {as : List α} (h : a ∈ as) (f : α → List α) :
f a <:+: flatMap f as
source
@[simp]
theorem List.map_eq_map {α β : Type u_2} (f : α → β) (l : List α) :
f <$> l = map f l
source
theorem List.comp_map {α : Type u} {β : Type v} {γ : Type w} (h : β → γ) (g : α → β) (l : List α) :
map (h ∘ g) l = map h (map g l)

A single `List.map` of a composition of functions is equal to composing a `List.map` with another `List.map`, fully applied. This is the reverse direction of `List.map_map`.

source
@[simp]
theorem List.map_comp_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) :
map g ∘ map f = map (g ∘ f)

Composing a `List.map` with another `List.map` is equal to a single `List.map` of composed functions.

source
theorem Function.LeftInverse.list_map {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : LeftInverse f g) :
LeftInverse (List.map f) (List.map g)
source
theorem Function.RightInverse.list_map {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : RightInverse f g) :
RightInverse (List.map f) (List.map g)
source
theorem Function.Involutive.list_map {α : Type u} {f : α → α} (h : Involutive f) :
Involutive (List.map f)
source
@[simp]
theorem List.map_leftInverse_iff {α : Type u} {β : Type v} {f : α → β} {g : β → α} :
Function.LeftInverse (map f) (map g) ↔ Function.LeftInverse f g
source
@[simp]
theorem List.map_rightInverse_iff {α : Type u} {β : Type v} {f : α → β} {g : β → α} :
Function.RightInverse (map f) (map g) ↔ Function.RightInverse f g
source
@[simp]
theorem List.map_involutive_iff {α : Type u} {f : α → α} :
Function.Involutive (map f) ↔ Function.Involutive f
source
theorem Function.Injective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Injective f) :
Injective (List.map f)
source
@[simp]
theorem List.map_injective_iff {α : Type u} {β : Type v} {f : α → β} :
Function.Injective (map f) ↔ Function.Injective f
source
theorem Function.Surjective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Surjective f) :
Surjective (List.map f)
source
@[simp]
theorem List.map_surjective_iff {α : Type u} {β : Type v} {f : α → β} :
Function.Surjective (map f) ↔ Function.Surjective f
source
theorem Function.Bijective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Bijective f) :
Bijective (List.map f)
source
@[simp]
theorem List.map_bijective_iff {α : Type u} {β : Type v} {f : α → β} :
Function.Bijective (map f) ↔ Function.Bijective f
source
theorem List.eq_of_mem_map_const {α : Type u} {β : Type v} {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (Function.const α b₂) l) :
b₁ = b₂
source
theorem List.eq_nil_or_concat' {α : Type u} (l : List α) :
l = [] ∨ ∃ (L : List α), ∃ (b : α), l = L ++ [b]

`eq_nil_or_concat` in simp normal form

### foldl, foldr #

source
theorem List.foldl_ext {α : Type u} {β : Type v} (f g : α → β → α) (a : α) {l : List β} (H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b) :
foldl f a l = foldl g a l
source
theorem List.foldr_ext {α : Type u} {β : Type v} (f g : α → β → β) (b : β) {l : List α} (H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b) :
foldr f b l = foldr g b l
source
theorem List.foldl_concat {α : Type u} {β : Type v} (f : β → α → β) (b : β) (x : α) (xs : List α) :
foldl f b (xs ++ [x]) = f (foldl f b xs) x
source
theorem List.foldr_concat {α : Type u} {β : Type v} (f : α → β → β) (b : β) (x : α) (xs : List α) :
foldr f b (xs ++ [x]) = foldr f (f x b) xs
source
theorem List.foldl_fixed' {α : Type u} {β : Type v} {f : α → β → α} {a : α} (hf : ∀ (b : β), f a b = a) (l : List β) :
foldl f a l = a
source
theorem List.foldr_fixed' {α : Type u} {β : Type v} {f : α → β → β} {b : β} (hf : ∀ (a : α), f a b = b) (l : List α) :
foldr f b l = b
source
@[simp]
theorem List.foldl_fixed {α : Type u} {β : Type v} {a : α} (l : List β) :
foldl (fun (a : α) (x : β) => a) a l = a
source
@[simp]
theorem List.foldr_fixed {α : Type u} {β : Type v} {b : β} (l : List α) :
foldr (fun (x : α) (b : β) => b) b l = b
source
theorem List.reverse_foldl {α : Type u} {l : List α} :
(foldl (fun (t : List α) (h : α) => h :: t) [] l).reverse = l
source
theorem List.foldl_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : α → β → γ) (op₁ : α → ι → α) (op₂ : β → ι → β) (op₃ : γ → ι → γ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i) :
foldl op₃ (f a b) l = f (foldl op₁ a l) (foldl op₂ b l)
source
theorem List.foldr_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : α → β → γ) (op₁ : ι → α → α) (op₂ : ι → β → β) (op₃ : ι → γ → γ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)) :
foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
source
theorem List.injective_foldl_comp {α : Type u} {l : List (α → α)} {f : α → α} (hl : ∀ (f : α → α), f ∈ l → Function.Injective f) (hf : Function.Injective f) :
Function.Injective (foldl Function.comp f l)
source
theorem List.append_cons_inj_of_notMem {α : Type u} {x₁ x₂ z₁ z₂ : List α} {a₁ a₂ : α} (notin_x : ¬a₂ ∈ x₁) (notin_z : ¬a₂ ∈ z₁) :
x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Consider two lists `l₁` and `l₂` with designated elements `a₁` and `a₂` somewhere in them: `l₁ = x₁ ++ [a₁] ++ z₁` and `l₂ = x₂ ++ [a₂] ++ z₂`. Assume the designated element `a₂` is present in neither `x₁` nor `z₁`. We conclude that the lists are equal (`l₁ = l₂`) if and only if their respective parts are equal (`x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂`).

source
@[deprecated List.append_cons_inj_of_notMem (since := "2025-05-23")]
theorem List.append_cons_inj_of_not_mem {α : Type u} {x₁ x₂ z₁ z₂ : List α} {a₁ a₂ : α} (notin_x : ¬a₂ ∈ x₁) (notin_z : ¬a₂ ∈ z₁) :
x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Alias of `List.append_cons_inj_of_notMem`.

Consider two lists `l₁` and `l₂` with designated elements `a₁` and `a₂` somewhere in them: `l₁ = x₁ ++ [a₁] ++ z₁` and `l₂ = x₂ ++ [a₂] ++ z₂`. Assume the designated element `a₂` is present in neither `x₁` nor `z₁`. We conclude that the lists are equal (`l₁ = l₂`) if and only if their respective parts are equal (`x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂`).

source
theorem List.foldl1_eq_foldr1 {α : Type u} {f : α → α → α} [hassoc : Std.Associative f] (a b : α) (l : List α) :
foldl f a (l ++ [b]) = foldr f b (a :: l)
source
theorem List.foldl_eq_of_comm_of_assoc {α : Type u} {f : α → α → α} [hcomm : Std.Commutative f] [hassoc : Std.Associative f] (a b : α) (l : List α) :
foldl f a (b :: l) = f b (foldl f a l)
source
theorem List.foldl_eq_foldr {α : Type u} {f : α → α → α} [Std.Commutative f] [Std.Associative f] (a : α) (l : List α) :
foldl f a l = foldr f a l
source
theorem List.foldl_eq_of_comm' {α : Type u} {β : Type v} {f : α → β → α} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (b : β) (l : List β) :
foldl f a (b :: l) = f (foldl f a l) b
source
theorem List.foldl_eq_foldr' {α : Type u} {β : Type v} {f : α → β → α} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (l : List β) :
foldl f a l = foldr (flip f) a l
source
theorem List.foldr_eq_of_comm' {α : Type u} {β : Type v} {f : α → β → β} (hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)) (a : β) (b : α) (l : List α) :
foldr f a (b :: l) = foldr f (f b a) l
source
theorem List.foldl_op_eq_op_foldr_assoc {α : Type u} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α} :
op (foldl op a₁ l) a₂ = op a₁ (foldr (fun (x1 x2 : α) => op x1 x2) a₂ l)
source
theorem List.foldl_assoc_comm_cons {α : Type u} {op : α → α → α} [ha : Std.Associative op] [hc : Std.Commutative op] {l : List α} {a₁ a₂ : α} :
foldl op a₂ (a₁ :: l) = op a₁ (foldl op a₂ l)

### foldlM, foldrM, mapM #

source
theorem List.foldrM_eq_foldr {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : α → β → m β) (b : β) (l : List α) :
foldrM f b l = foldr (fun (a : α) (mb : m β) => mb >>= f a) (pure b) l
source
theorem List.foldlM_eq_foldl {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : β → α → m β) (b : β) (l : List α) :
foldlM f b l = foldl (fun (mb : m β) (a : α) => do let b ← mb f b a) (pure b) l

### filter #

source
theorem List.length_eq_length_filter_add {α : Type u} {l : List α} (f : α → Bool) :
l.length = (filter f l).length + (filter (fun (x : α) => !f x) l).length

### filterMap #

source
theorem List.filterMap_eq_flatMap_toList {α : Type u} {β : Type v} (f : α → Option β) (l : List α) :
filterMap f l = flatMap (fun (a : α) => (f a).toList) l
source
theorem List.filterMap_congr {α : Type u} {β : Type v} {f g : α → Option β} {l : List α} (h : ∀ (x : α), x ∈ l → f x = g x) :
filterMap f l = filterMap g l
source
theorem List.filterMap_eq_map_iff_forall_eq_some {α : Type u} {β : Type v} {f : α → Option β} {g : α → β} {l : List α} :
filterMap f l = map g l ↔ ∀ (x : α), x ∈ l → f x = some (g x)

### filter #

source
theorem List.filter_singleton {α : Type u} {p : α → Bool} {a : α} :
filter p [a] = bif p a then [a] else []
source
theorem List.filter_eq_foldr {α : Type u} (p : α → Bool) (l : List α) :
filter p l = foldr (fun (a : α) (out : List α) => bif p a then a :: out else out) [] l
source
@[simp]
theorem List.filter_subset' {α : Type u} {p : α → Bool} (l : List α) :
filter p l ⊆ l
source
theorem List.of_mem_filter {α : Type u} {p : α → Bool} {a : α} {l : List α} (h : a ∈ filter p l) :
p a = true
source
theorem List.mem_of_mem_filter {α : Type u} {p : α → Bool} {a : α} {l : List α} (h : a ∈ filter p l) :
a ∈ l
source
theorem List.mem_filter_of_mem {α : Type u} {p : α → Bool} {a : α} {l : List α} (h₁ : a ∈ l) (h₂ : p a = true) :
a ∈ filter p l
source
theorem List.monotone_filter_right {α : Type u} (l : List α) ⦃p q : α → Bool⦄ (h : ∀ (a : α), p a = true → q a = true) :
(filter p l).Sublist (filter q l)
source
theorem List.map_filter {α : Type u} {β : Type v} (p : α → Bool) {f : α → β} (hf : Function.Injective f) (l : List α) [DecidablePred fun (b : β) => ∃ (a : α), p a = true ∧ f a = b] :
map f (filter p l) = filter (fun (b : β) => decide (∃ (a : α), p a = true ∧ f a = b)) (map f l)
source
theorem List.filter_attach' {α : Type u} (l : List α) (p : { a : α // a ∈ l } → Bool) [DecidableEq α] :
filter p l.attach = map (Subtype.map id ⋯) (filter (fun (x : α) => decide (∃ (h : x ∈ l), p ⟨x, h⟩ = true)) l).attach
source
theorem List.filter_attach {α : Type u} (l : List α) (p : α → Bool) :
filter (fun (x : { x : α // x ∈ l }) => p ↑x) l.attach = map (Subtype.map id ⋯) (filter p l).attach
source
theorem List.filter_comm {α : Type u} (p q : α → Bool) (l : List α) :
filter p (filter q l) = filter q (filter p l)
source
@[simp]
theorem List.filter_true {α : Type u} (l : List α) :
filter (fun (x : α) => true) l = l
source
@[simp]
theorem List.filter_false {α : Type u} (l : List α) :
filter (fun (x : α) => false) l = []

### eraseP #

source
theorem List.length_eraseP_add_one {α : Type u} {p : α → Bool} {l : List α} {a : α} (al : a ∈ l) (pa : p a = true) :
(eraseP p l).length + 1 = l.length

### erase #

source
theorem List.length_erase_add_one {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) :
(l.erase a).length + 1 = l.length
source
theorem List.map_erase {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {a : α} (l : List α) :
map f (l.erase a) = (map f l).erase (f a)
source
theorem List.map_foldl_erase {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {l₁ l₂ : List α} :
map f (foldl List.erase l₁ l₂) = foldl (fun (l : List β) (a : α) => l.erase (f a)) (map f l₁) l₂
source
theorem List.erase_getElem {ι : Type u_1} [DecidableEq ι] {l : List ι} {i : ℕ} (hi : i < l.length) :
(l.erase l[i]).Perm (l.eraseIdx i)
source
theorem List.length_eraseIdx_add_one {ι : Type u_1} {l : List ι} {i : ℕ} (h : i < l.length) :
(l.eraseIdx i).length + 1 = l.length

### diff #

source
@[simp]
theorem List.map_diff {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {l₁ l₂ : List α} :
map f (l₁.diff l₂) = (map f l₁).diff (map f l₂)
source
theorem List.choose_spec {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) :
choose p l hp ∈ l ∧ p (choose p l hp)
source
theorem List.choose_mem {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) :
choose p l hp ∈ l
source
theorem List.choose_property {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) :
p (choose p l hp)

### Forall #

source
@[simp]
theorem List.forall_cons {α : Type u} (p : α → Prop) (x : α) (l : List α) :
Forall p (x :: l) ↔ p x ∧ Forall p l
source
@[simp]
theorem List.forall_append {α : Type u} {p : α → Prop} {xs ys : List α} :
Forall p (xs ++ ys) ↔ Forall p xs ∧ Forall p ys
source
theorem List.forall_iff_forall_mem {α : Type u} {p : α → Prop} {l : List α} :
Forall p l ↔ ∀ (x : α), x ∈ l → p x
source
theorem List.Forall.imp {α : Type u} {p q : α → Prop} (h : ∀ (x : α), p x → q x) {l : List α} :
Forall p l → Forall q l
source
@[simp]
theorem List.forall_map_iff {α : Type u} {β : Type v} {l : List α} {p : β → Prop} (f : α → β) :
Forall p (map f l) ↔ Forall (p ∘ f) l
source
instance List.instDecidablePredForall {α : Type u} (p : α → Prop) [DecidablePred p] :
DecidablePred (Forall p)
Equations

- List.instDecidablePredForall p x✝ = decidable_of_iff' (∀ (x : α), x ∈ x✝ → p x) ⋯

### Miscellaneous lemmas #

source
theorem List.get_attach {α : Type u} (l : List α) (i : Fin l.attach.length) :
↑(l.attach.get i) = l.get ⟨↑i, ⋯⟩
source
theorem List.disjoint_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s t : List α} (hs : ∀ (a : α), a ∈ s → p a) (ht : ∀ (a : α), a ∈ t → p a) (hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a') (h : s.Disjoint t) :
(pmap f s hs).Disjoint (pmap f t ht)

The images of disjoint lists under a partially defined map are disjoint

source
theorem List.disjoint_map {α : Type u} {β : Type v} {f : α → β} {s t : List α} (hf : Function.Injective f) (h : s.Disjoint t) :
(map f s).Disjoint (map f t)

The images of disjoint lists under an injective map are disjoint

source
theorem List.Disjoint.map {α : Type u} {β : Type v} {f : α → β} {s t : List α} (hf : Function.Injective f) (h : s.Disjoint t) :
(List.map f s).Disjoint (List.map f t)

Alias of `List.disjoint_map`.

The images of disjoint lists under an injective map are disjoint

source
theorem List.Disjoint.of_map {α : Type u} {β : Type v} {f : α → β} {s t : List α} (h : (List.map f s).Disjoint (List.map f t)) :
s.Disjoint t
source
theorem List.Disjoint.map_iff {α : Type u} {β : Type v} {f : α → β} {s t : List α} (hf : Function.Injective f) :
(List.map f s).Disjoint (List.map f t) ↔ s.Disjoint t
source
theorem List.Perm.disjoint_left {α : Type u} {l₁ l₂ l : List α} (p : l₁.Perm l₂) :
l₁.Disjoint l ↔ l₂.Disjoint l
source
theorem List.Perm.disjoint_right {α : Type u} {l₁ l₂ l : List α} (p : l₁.Perm l₂) :
l.Disjoint l₁ ↔ l.Disjoint l₂
source
@[simp]
theorem List.disjoint_reverse_left {α : Type u} {l₁ l₂ : List α} :
l₁.reverse.Disjoint l₂ ↔ l₁.Disjoint l₂
source
@[simp]
theorem List.disjoint_reverse_right {α : Type u} {l₁ l₂ : List α} :
l₁.Disjoint l₂.reverse ↔ l₁.Disjoint l₂
source
theorem List.lookup_graph {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] (f : α → β) {a : α} {as : List α} (h : a ∈ as) :
lookup a (map (fun (x : α) => (x, f x)) as) = some (f a)
source
@[simp]
theorem List.range'_0 (a b : ℕ) :
range' a b 0 = replicate b a
source
theorem List.left_le_of_mem_range' {a b s x : ℕ} (hx : x ∈ range' a b s) :
a ≤ x