mathlib docs: data.list.basic

Induction principle from the right for lists: if a property holds for the empty list, and for l ++ [a] if it holds for l, then it holds for all lists. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations

l.reverse_rec_on H0 H1 = _.mpr (list.rec H0 (λ (hd : α) (tl : list α) (ih : C tl.reverse), _.mpr (H1 tl.reverse hd ih)) l.reverse)

source

def list.bidirectional_rec {α : Type u} {C : list α → Sort u_1} (H0 : C list.nil) (H1 : Π (a : α), C [a]) (Hn : Π (a : α) (l : list α) (b : α), C l → C (a :: (l ++ [b]))) (l : list α) :

C l

Bidirectional induction principle for lists: if a property holds for the empty list, the singleton list, and a :: (l ++ [b]) from l, then it holds for all lists. This can be used to prove statements about palindromes. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations

list.bidirectional_rec H0 H1 Hn (a :: b :: l) = let l' : list α := (b :: l).init, b' : α := (b :: l).last _ in _.mpr (Hn a l' b' (list.bidirectional_rec H0 H1 Hn l'))
list.bidirectional_rec H0 H1 Hn [a] = H1 a
list.bidirectional_rec H0 H1 Hn list.nil = H0

source

def list.bidirectional_rec_on {α : Type u} {C : list α → Sort u_1} (l : list α) :

C list.nil → (Π (a : α), C [a]) → (Π (a : α) (l : list α) (b : α), C l → C (a :: (l ++ [b]))) → C l

Like bidirectional_rec, but with the list parameter placed first.

Equations

l.bidirectional_rec_on H0 H1 Hn = list.bidirectional_rec H0 H1 Hn l

source

@[simp]

theorem list.nil_sublist {α : Type u} (l : list α) :

list.nil <+ l

source

@[simp]

theorem list.sublist.refl {α : Type u} (l : list α) :

l <+ l

source

theorem list.sublist.trans {α : Type u} {l₁ l₂ l₃ : list α} :

l₁ <+ l₂ → l₂ <+ l₃ → l₁ <+ l₃

source

@[simp]

theorem list.sublist_cons {α : Type u} (a : α) (l : list α) :

l <+ a :: l

source

theorem list.sublist_of_cons_sublist {α : Type u} {a : α} {l₁ l₂ : list α} :

a :: l₁ <+ l₂ → l₁ <+ l₂

source

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

l₁ <+ l₂ → a :: l₁ <+ a :: l₂

source

@[simp]

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

l₁ <+ l₁ ++ l₂

source

@[simp]

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

l₂ <+ l₁ ++ l₂

source

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

l₁ <+ l₂ → l₁ <+ a :: l₂

source

theorem list.sublist_append_of_sublist_left {α : Type u} {l l₁ l₂ : list α} :

l <+ l₁ → l <+ l₁ ++ l₂

source

theorem list.sublist_append_of_sublist_right {α : Type u} {l l₁ l₂ : list α} :

l <+ l₂ → l <+ l₁ ++ l₂

source

theorem list.sublist_of_cons_sublist_cons {α : Type u} {l₁ l₂ : list α} {a : α} :

a :: l₁ <+ a :: l₂ → l₁ <+ l₂

source

theorem list.cons_sublist_cons_iff {α : Type u} {l₁ l₂ : list α} {a : α} :

a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂

source

@[simp]

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

l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂

source

theorem list.sublist.append_right {α : Type u} {l₁ l₂ : list α} (h : l₁ <+ l₂) (l : list α) :

l₁ ++ l <+ l₂ ++ l

source

theorem list.sublist_or_mem_of_sublist {α : Type u} {l l₁ l₂ : list α} {a : α} :

l <+ l₁ ++ a :: l₂ → l <+ l₁ ++ l₂ ∨ a ∈ l

source

theorem list.sublist.reverse {α : Type u} {l₁ l₂ : list α} :

l₁ <+ l₂ → l₁.reverse <+ l₂.reverse

source

@[simp]

theorem list.reverse_sublist_iff {α : Type u} {l₁ l₂ : list α} :

l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂

source

@[simp]

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

l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂

source

theorem list.sublist.append {α : Type u} {l₁ l₂ r₁ r₂ : list α} :

l₁ <+ l₂ → r₁ <+ r₂ → l₁ ++ r₁ <+ l₂ ++ r₂

source

theorem list.sublist.subset {α : Type u} {l₁ l₂ : list α} :

l₁ <+ l₂ → l₁ ⊆ l₂

source

theorem list.singleton_sublist {α : Type u} {a : α} {l : list α} :

[a] <+ l ↔ a ∈ l

source

theorem list.eq_nil_of_sublist_nil {α : Type u} {l : list α} :

l <+ list.nil → l = list.nil

source

theorem list.repeat_sublist_repeat {α : Type u} (a : α) {m n : ℕ} :

list.repeat a m <+ list.repeat a n ↔ m ≤ n

source

theorem list.eq_of_sublist_of_length_eq {α : Type u} {l₁ l₂ : list α} :

l₁ <+ l₂ → l₁.length = l₂.length → l₁ = l₂

source

theorem list.eq_of_sublist_of_length_le {α : Type u} {l₁ l₂ : list α} :

l₁ <+ l₂ → l₂.length ≤ l₁.length → l₁ = l₂

source

theorem list.sublist.antisymm {α : Type u} {l₁ l₂ : list α} :

l₁ <+ l₂ → l₂ <+ l₁ → l₁ = l₂

source

@[instance]

def list.decidable_sublist {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

decidable (l₁ <+ l₂)

Equations

(a :: l₁).decidable_sublist (b :: l₂) = dite (a = b) (λ (h : a = b), decidable_of_decidable_of_iff (l₁.decidable_sublist l₂) _) (λ (h : ¬a = b), decidable_of_decidable_of_iff ((a :: l₁).decidable_sublist l₂) _)
(a :: l₁).decidable_sublist list.nil = decidable.is_false _
list.nil.decidable_sublist (hd :: tl) = decidable.is_true _
list.nil.decidable_sublist list.nil = decidable.is_true list.decidable_sublist._main._proof_1

source

@[simp]

theorem list.index_of_nil {α : Type u} [decidable_eq α] (a : α) :

list.index_of a list.nil = 0

source

theorem list.index_of_cons {α : Type u} [decidable_eq α] (a b : α) (l : list α) :

list.index_of a (b :: l) = ite (a = b) 0 (list.index_of a l).succ

source

theorem list.index_of_cons_eq {α : Type u} [decidable_eq α] {a b : α} (l : list α) :

a = b → list.index_of a (b :: l) = 0

source

@[simp]

theorem list.index_of_cons_self {α : Type u} [decidable_eq α] (a : α) (l : list α) :

list.index_of a (a :: l) = 0

source

@[simp]

theorem list.index_of_cons_ne {α : Type u} [decidable_eq α] {a b : α} (l : list α) :

a ≠ b → list.index_of a (b :: l) = (list.index_of a l).succ

source

theorem list.index_of_eq_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :

list.index_of a l = l.length ↔ a ∉ l

source

@[simp]

theorem list.index_of_of_not_mem {α : Type u} [decidable_eq α] {l : list α} {a : α} :

a ∉ l → list.index_of a l = l.length

source

theorem list.index_of_le_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :

list.index_of a l ≤ l.length

source

theorem list.index_of_lt_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :

list.index_of a l < l.length ↔ a ∈ l

source

theorem list.nth_le_of_mem {α : Type u} {a : α} {l : list α} :

a ∈ l → (∃ (n : ℕ) (h : n < l.length), l.nth_le n h = a)

source

theorem list.nth_le_nth {α : Type u} {l : list α} {n : ℕ} (h : n < l.length) :

l.nth n = option.some (l.nth_le n h)

source

theorem list.nth_len_le {α : Type u} {l : list α} {n : ℕ} :

l.length ≤ n → l.nth n = option.none

source

theorem list.nth_eq_some {α : Type u} {l : list α} {n : ℕ} {a : α} :

l.nth n = option.some a ↔ ∃ (h : n < l.length), l.nth_le n h = a

source

theorem list.nth_of_mem {α : Type u} {a : α} {l : list α} :

a ∈ l → (∃ (n : ℕ), l.nth n = option.some a)

source

theorem list.nth_le_mem {α : Type u} (l : list α) (n : ℕ) (h : n < l.length) :

l.nth_le n h ∈ l

source

theorem list.nth_mem {α : Type u} {l : list α} {n : ℕ} {a : α} :

l.nth n = option.some a → a ∈ l

source

theorem list.mem_iff_nth_le {α : Type u} {a : α} {l : list α} :

a ∈ l ↔ ∃ (n : ℕ) (h : n < l.length), l.nth_le n h = a

source

theorem list.mem_iff_nth {α : Type u} {a : α} {l : list α} :

a ∈ l ↔ ∃ (n : ℕ), l.nth n = option.some a

source

@[simp]

theorem list.nth_map {α : Type u} {β : Type v} (f : α → β) (l : list α) (n : ℕ) :

(list.map f l).nth n = option.map f (l.nth n)

source

theorem list.nth_le_map {α : Type u} {β : Type v} (f : α → β) {l : list α} {n : ℕ} (H1 : n < (list.map f l).length) (H2 : n < l.length) :

(list.map f l).nth_le n H1 = f (l.nth_le n H2)

source

theorem list.nth_le_map_rev {α : Type u} {β : Type v} (f : α → β) {l : list α} {n : ℕ} (H : n < l.length) :

f (l.nth_le n H) = (list.map f l).nth_le n _

A version of nth_le_map that can be used for rewriting.

source

@[simp]

theorem list.nth_le_map' {α : Type u} {β : Type v} (f : α → β) {l : list α} {n : ℕ} (H : n < (list.map f l).length) :

(list.map f l).nth_le n H = f (l.nth_le n _)

source

theorem list.nth_le_of_eq {α : Type u} {L L' : list α} (h : L = L') {i : ℕ} (hi : i < L.length) :

L.nth_le i hi = L'.nth_le i _

If one has nth_le L i hi in a formula and h : L = L', one can not rw h in the formula as hi gives i < L.length and not i < L'.length. The lemma nth_le_of_eq can be used to make such a rewrite, with rw (nth_le_of_eq h).

source

@[simp]

theorem list.nth_le_singleton {α : Type u} (a : α) {n : ℕ} (hn : n < 1) :

[a].nth_le n hn = a

source

theorem list.nth_le_zero {α : Type u} [inhabited α] {L : list α} (h : 0 < L.length) :

L.nth_le 0 h = L.head

source

theorem list.nth_le_append {α : Type u} {l₁ l₂ : list α} {n : ℕ} (hn₁ : n < (l₁ ++ l₂).length) (hn₂ : n < l₁.length) :

(l₁ ++ l₂).nth_le n hn₁ = l₁.nth_le n hn₂

source

theorem list.nth_le_append_right_aux {α : Type u} {l₁ l₂ : list α} {n : ℕ} :

l₁.length ≤ n → n < (l₁ ++ l₂).length → n - l₁.length < l₂.length

source

theorem list.nth_le_append_right {α : Type u} {l₁ l₂ : list α} {n : ℕ} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) :

(l₁ ++ l₂).nth_le n h₂ = l₂.nth_le (n - l₁.length) _

source

@[simp]

theorem list.nth_le_repeat {α : Type u} (a : α) {n m : ℕ} (h : m < (list.repeat a n).length) :

(list.repeat a n).nth_le m h = a

source

theorem list.nth_append {α : Type u} {l₁ l₂ : list α} {n : ℕ} :

n < l₁.length → (l₁ ++ l₂).nth n = l₁.nth n

source

theorem list.last_eq_nth_le {α : Type u} (l : list α) (h : l ≠ list.nil) :

l.last h = l.nth_le (l.length - 1) _

source

@[simp]

theorem list.nth_concat_length {α : Type u} (l : list α) (a : α) :

(l ++ [a]).nth l.length = option.some a

source

@[ext]

theorem list.ext {α : Type u} {l₁ l₂ : list α} :

(∀ (n : ℕ), l₁.nth n = l₂.nth n) → l₁ = l₂

source

theorem list.ext_le {α : Type u} {l₁ l₂ : list α} :

l₁.length = l₂.length → (∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.nth_le n h₁ = l₂.nth_le n h₂) → l₁ = l₂

source

@[simp]

theorem list.index_of_nth_le {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : list.index_of a l < l.length) :

l.nth_le (list.index_of a l) h = a

source

@[simp]

theorem list.index_of_nth {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∈ l → l.nth (list.index_of a l) = option.some a

source

theorem list.nth_le_reverse_aux1 {α : Type u} (l r : list α) (i : ℕ) (h1 : i + l.length < (l.reverse_core r).length) (h2 : i < r.length) :

(l.reverse_core r).nth_le (i + l.length) h1 = r.nth_le i h2

source

theorem list.index_of_inj {α : Type u} [decidable_eq α] {l : list α} {x y : α} :

x ∈ l → y ∈ l → (list.index_of x l = list.index_of y l ↔ x = y)

source

theorem list.nth_le_reverse_aux2 {α : Type u} (l r : list α) (i : ℕ) (h1 : l.length - 1 - i < (l.reverse_core r).length) (h2 : i < l.length) :

(l.reverse_core r).nth_le (l.length - 1 - i) h1 = l.nth_le i h2

source

@[simp]

theorem list.nth_le_reverse {α : Type u} (l : list α) (i : ℕ) (h1 : l.length - 1 - i < l.reverse.length) (h2 : i < l.length) :

l.reverse.nth_le (l.length - 1 - i) h1 = l.nth_le i h2

source

theorem list.eq_cons_of_length_one {α : Type u} {l : list α} (h : l.length = 1) :

l = [l.nth_le 0 _]

source

theorem list.modify_nth_tail_modify_nth_tail {α : Type u} {f g : list α → list α} (m n : ℕ) (l : list α) :

list.modify_nth_tail g (m + n) (list.modify_nth_tail f n l) = list.modify_nth_tail (λ (l : list α), list.modify_nth_tail g m (f l)) n l

source

theorem list.modify_nth_tail_modify_nth_tail_le {α : Type u} {f g : list α → list α} (m n : ℕ) (l : list α) :

n ≤ m → list.modify_nth_tail g m (list.modify_nth_tail f n l) = list.modify_nth_tail (λ (l : list α), list.modify_nth_tail g (m - n) (f l)) n l

source

theorem list.modify_nth_tail_modify_nth_tail_same {α : Type u} {f g : list α → list α} (n : ℕ) (l : list α) :

list.modify_nth_tail g n (list.modify_nth_tail f n l) = list.modify_nth_tail (g ∘ f) n l

source

theorem list.modify_nth_tail_id {α : Type u} (n : ℕ) (l : list α) :

list.modify_nth_tail id n l = l

source

theorem list.remove_nth_eq_nth_tail {α : Type u} (n : ℕ) (l : list α) :

l.remove_nth n = list.modify_nth_tail list.tail n l

source

theorem list.update_nth_eq_modify_nth {α : Type u} (a : α) (n : ℕ) (l : list α) :

l.update_nth n a = list.modify_nth (λ (_x : α), a) n l

source

theorem list.modify_nth_eq_update_nth {α : Type u} (f : α → α) (n : ℕ) (l : list α) :

list.modify_nth f n l = ((λ (a : α), l.update_nth n (f a)) <$> l.nth n).get_or_else l

source

theorem list.nth_modify_nth {α : Type u} (f : α → α) (n : ℕ) (l : list α) (m : ℕ) :

(list.modify_nth f n l).nth m = (λ (a : α), ite (n = m) (f a) a) <$> l.nth m

source

theorem list.modify_nth_tail_length {α : Type u} (f : list α → list α) (H : ∀ (l : list α), (f l).length = l.length) (n : ℕ) (l : list α) :

(list.modify_nth_tail f n l).length = l.length

source

@[simp]

theorem list.modify_nth_length {α : Type u} (f : α → α) (n : ℕ) (l : list α) :

(list.modify_nth f n l).length = l.length

source

@[simp]

theorem list.update_nth_length {α : Type u} (l : list α) (n : ℕ) (a : α) :

(l.update_nth n a).length = l.length

source

@[simp]

theorem list.nth_modify_nth_eq {α : Type u} (f : α → α) (n : ℕ) (l : list α) :

(list.modify_nth f n l).nth n = f <$> l.nth n

source

@[simp]

theorem list.nth_modify_nth_ne {α : Type u} (f : α → α) {m n : ℕ} (l : list α) :

m ≠ n → (list.modify_nth f m l).nth n = l.nth n

source

theorem list.nth_update_nth_eq {α : Type u} (a : α) (n : ℕ) (l : list α) :

(l.update_nth n a).nth n = (λ (_x : α), a) <$> l.nth n

source

theorem list.nth_update_nth_of_lt {α : Type u} (a : α) {n : ℕ} {l : list α} :

n < l.length → (l.update_nth n a).nth n = option.some a

source

theorem list.nth_update_nth_ne {α : Type u} (a : α) {m n : ℕ} (l : list α) :

m ≠ n → (l.update_nth m a).nth n = l.nth n

source

@[simp]

theorem list.nth_le_update_nth_eq {α : Type u} (l : list α) (i : ℕ) (a : α) (h : i < (l.update_nth i a).length) :

(l.update_nth i a).nth_le i h = a

source

@[simp]

theorem list.nth_le_update_nth_of_ne {α : Type u} {l : list α} {i j : ℕ} (h : i ≠ j) (a : α) (hj : j < (l.update_nth i a).length) :

(l.update_nth i a).nth_le j hj = l.nth_le j _

source

theorem list.mem_or_eq_of_mem_update_nth {α : Type u} {l : list α} {n : ℕ} {a b : α} :

a ∈ l.update_nth n b → a ∈ l ∨ a = b

source

@[simp]

theorem list.insert_nth_nil {α : Type u} (a : α) :

list.insert_nth 0 a list.nil = [a]

source

theorem list.length_insert_nth {α : Type u} {a : α} (n : ℕ) (as : list α) :

n ≤ as.length → (list.insert_nth n a as).length = as.length + 1

source

theorem list.remove_nth_insert_nth {α : Type u} {a : α} (n : ℕ) (l : list α) :

(list.insert_nth n a l).remove_nth n = l

source

theorem list.insert_nth_remove_nth_of_ge {α : Type u} {a : α} (n m : ℕ) (as : list α) :

n < as.length → n ≤ m → list.insert_nth m a (as.remove_nth n) = (list.insert_nth (m + 1) a as).remove_nth n

source

theorem list.insert_nth_remove_nth_of_le {α : Type u} {a : α} (n m : ℕ) (as : list α) :

n < as.length → m ≤ n → list.insert_nth m a (as.remove_nth n) = (list.insert_nth m a as).remove_nth (n + 1)

source

theorem list.insert_nth_comm {α : Type u} (a b : α) (i j : ℕ) (l : list α) :

i ≤ j → j ≤ l.length → list.insert_nth (j + 1) b (list.insert_nth i a l) = list.insert_nth i a (list.insert_nth j b l)

source

theorem list.mem_insert_nth {α : Type u} {a b : α} {n : ℕ} {l : list α} :

n ≤ l.length → (a ∈ list.insert_nth n b l ↔ a = b ∨ a ∈ l)

source

@[simp]

theorem list.map_nil {α : Type u} {β : Type v} (f : α → β) :

list.map f list.nil = list.nil

source

theorem list.map_eq_foldr {α : Type u} {β : Type v} (f : α → β) (l : list α) :

list.map f l = list.foldr (λ (a : α) (bs : list β), f a :: bs) list.nil l

source

theorem list.map_congr {α : Type u} {β : Type v} {f g : α → β} {l : list α} :

(∀ (x : α), x ∈ l → f x = g x) → list.map f l = list.map g l

source

theorem list.map_eq_map_iff {α : Type u} {β : Type v} {f g : α → β} {l : list α} :

list.map f l = list.map g l ↔ ∀ (x : α), x ∈ l → f x = g x

source

theorem list.map_concat {α : Type u} {β : Type v} (f : α → β) (a : α) (l : list α) :

list.map f (l.concat a) = (list.map f l).concat (f a)

source

theorem list.map_id' {α : Type u} {f : α → α} (h : ∀ (x : α), f x = x) (l : list α) :

list.map f l = l

source

theorem list.eq_nil_of_map_eq_nil {α : Type u} {β : Type v} {f : α → β} {l : list α} :

list.map f l = list.nil → l = list.nil

source

@[simp]

theorem list.map_join {α : Type u} {β : Type v} (f : α → β) (L : list (list α)) :

list.map f L.join = (list.map (list.map f) L).join

source

theorem list.bind_ret_eq_map {α : Type u} {β : Type v} (f : α → β) (l : list α) :

l.bind (list.ret ∘ f) = list.map f l

source

@[simp]

theorem list.map_eq_map {α β : Type u_1} (f : α → β) (l : list α) :

f <$> l = list.map f l

source

@[simp]

theorem list.map_tail {α : Type u} {β : Type v} (f : α → β) (l : list α) :

list.map f l.tail = (list.map f l).tail

source

@[simp]

theorem list.map_injective_iff {α : Type u} {β : Type v} {f : α → β} :

function.injective (list.map f) ↔ function.injective f

source

theorem list.map_filter_eq_foldr {α : Type u} {β : Type v} (f : α → β) (p : α → Prop) [decidable_pred p] (as : list α) :

list.map f (list.filter p as) = list.foldr (λ (a : α) (bs : list β), ite (p a) (f a :: bs) bs) list.nil as

source

theorem list.nil_map₂ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : list β) :

list.map₂ f list.nil l = list.nil

source

theorem list.map₂_nil {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : list α) :

list.map₂ f l list.nil = list.nil

source

@[simp]

theorem list.take_zero {α : Type u} (l : list α) :

list.take 0 l = list.nil

source

@[simp]

theorem list.take_nil {α : Type u} (n : ℕ) :

list.take n list.nil = list.nil

source

theorem list.take_cons {α : Type u} (n : ℕ) (a : α) (l : list α) :

list.take n.succ (a :: l) = a :: list.take n l

source

@[simp]

theorem list.take_length {α : Type u} (l : list α) :

list.take l.length l = l

source

theorem list.take_all_of_le {α : Type u} {n : ℕ} {l : list α} :

l.length ≤ n → list.take n l = l

source

@[simp]

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

list.take l₁.length (l₁ ++ l₂) = l₁

source

theorem list.take_left' {α : Type u} {l₁ l₂ : list α} {n : ℕ} :

l₁.length = n → list.take n (l₁ ++ l₂) = l₁

source

theorem list.take_take {α : Type u} (n m : ℕ) (l : list α) :

list.take n (list.take m l) = list.take (min n m) l

source

theorem list.take_repeat {α : Type u} (a : α) (n m : ℕ) :

list.take n (list.repeat a m) = list.repeat a (min n m)

source

theorem list.map_take {α : Type u_1} {β : Type u_2} (f : α → β) (L : list α) (i : ℕ) :

list.map f (list.take i L) = list.take i (list.map f L)

source

theorem list.take_append_of_le_length {α : Type u} {l₁ l₂ : list α} {n : ℕ} :

n ≤ l₁.length → list.take n (l₁ ++ l₂) = list.take n l₁

source

theorem list.take_append {α : Type u} {l₁ l₂ : list α} (i : ℕ) :

list.take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ list.take i l₂

Taking the first l₁.length + i elements in l₁ ++ l₂ is the same as appending the first i elements of l₂ to l₁.

source

theorem list.nth_le_take {α : Type u} (L : list α) {i j : ℕ} (hi : i < L.length) (hj : i < j) :

L.nth_le i hi = (list.take j L).nth_le i _

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the big list to the small list.

source

theorem list.nth_le_take' {α : Type u} (L : list α) {i j : ℕ} (hi : i < (list.take j L).length) :

(list.take j L).nth_le i hi = L.nth_le i _

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the small list to the big list.

source

@[simp]

theorem list.drop_nil {α : Type u} (n : ℕ) :

list.drop n list.nil = list.nil

source

@[simp]

theorem list.drop_one {α : Type u} (l : list α) :

list.drop 1 l = l.tail

source

theorem list.drop_add {α : Type u} (m n : ℕ) (l : list α) :

list.drop (m + n) l = list.drop m (list.drop n l)

source

@[simp]

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

list.drop l₁.length (l₁ ++ l₂) = l₂

source

theorem list.drop_left' {α : Type u} {l₁ l₂ : list α} {n : ℕ} :

l₁.length = n → list.drop n (l₁ ++ l₂) = l₂

source

theorem list.drop_eq_nth_le_cons {α : Type u} {n : ℕ} {l : list α} (h : n < l.length) :

list.drop n l = l.nth_le n h :: list.drop (n + 1) l

source

@[simp]

theorem list.drop_length {α : Type u} (l : list α) :

list.drop l.length l = list.nil

source

theorem list.drop_append_of_le_length {α : Type u} {l₁ l₂ : list α} {n : ℕ} :

n ≤ l₁.length → list.drop n (l₁ ++ l₂) = list.drop n l₁ ++ l₂

source

theorem list.drop_append {α : Type u} {l₁ l₂ : list α} (i : ℕ) :

list.drop (l₁.length + i) (l₁ ++ l₂) = list.drop i l₂

Dropping the elements up to l₁.length + i in l₁ + l₂ is the same as dropping the elements up to i in l₂.

source

theorem list.nth_le_drop {α : Type u} (L : list α) {i j : ℕ} (h : i + j < L.length) :

L.nth_le (i + j) h = (list.drop i L).nth_le j _

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the big list to the small list.

source

theorem list.nth_le_drop' {α : Type u} (L : list α) {i j : ℕ} (h : j < (list.drop i L).length) :

(list.drop i L).nth_le j h = L.nth_le (i + j) _

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the small list to the big list.

source

@[simp]

theorem list.drop_drop {α : Type u} (n m : ℕ) (l : list α) :

list.drop n (list.drop m l) = list.drop (n + m) l

source

theorem list.drop_take {α : Type u} (m n : ℕ) (l : list α) :

list.drop m (list.take (m + n) l) = list.take n (list.drop m l)

source

theorem list.map_drop {α : Type u_1} {β : Type u_2} (f : α → β) (L : list α) (i : ℕ) :

list.map f (list.drop i L) = list.drop i (list.map f L)

source

theorem list.modify_nth_tail_eq_take_drop {α : Type u} (f : list α → list α) (H : f list.nil = list.nil) (n : ℕ) (l : list α) :

list.modify_nth_tail f n l = list.take n l ++ f (list.drop n l)

source

theorem list.modify_nth_eq_take_drop {α : Type u} (f : α → α) (n : ℕ) (l : list α) :

list.modify_nth f n l = list.take n l ++ list.modify_head f (list.drop n l)

source

theorem list.modify_nth_eq_take_cons_drop {α : Type u} (f : α → α) {n : ℕ} {l : list α} (h : n < l.length) :

list.modify_nth f n l = list.take n l ++ f (l.nth_le n h) :: list.drop (n + 1) l

source

theorem list.update_nth_eq_take_cons_drop {α : Type u} (a : α) {n : ℕ} {l : list α} :

n < l.length → l.update_nth n a = list.take n l ++ a :: list.drop (n + 1) l

source

@[simp]

theorem list.update_nth_eq_nil {α : Type u} (l : list α) (n : ℕ) (a : α) :

l.update_nth n a = list.nil ↔ l = list.nil

source

@[simp]

theorem list.take'_length {α : Type u} [inhabited α] (n : ℕ) (l : list α) :

(list.take' n l).length = n

source

@[simp]

theorem list.take'_nil {α : Type u} [inhabited α] (n : ℕ) :

list.take' n list.nil = list.repeat (inhabited.default α) n

source

theorem list.take'_eq_take {α : Type u} [inhabited α] {n : ℕ} {l : list α} :

n ≤ l.length → list.take' n l = list.take n l

source

@[simp]

theorem list.take'_left {α : Type u} [inhabited α] (l₁ l₂ : list α) :

list.take' l₁.length (l₁ ++ l₂) = l₁

source

theorem list.take'_left' {α : Type u} [inhabited α] {l₁ l₂ : list α} {n : ℕ} :

l₁.length = n → list.take' n (l₁ ++ l₂) = l₁

source

theorem list.foldl_ext {α : Type u} {β : Type v} (f g : α → β → α) (a : α) {l : list β} :

(∀ (a : α) (b : β), b ∈ l → f a b = g a b) → list.foldl f a l = list.foldl g a l

source

theorem list.foldr_ext {α : Type u} {β : Type v} (f g : α → β → β) (b : β) {l : list α} :

(∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b) → list.foldr f b l = list.foldr g b l

source

@[simp]

theorem list.foldl_nil {α : Type u} {β : Type v} (f : α → β → α) (a : α) :

list.foldl f a list.nil = a

source

@[simp]

theorem list.foldl_cons {α : Type u} {β : Type v} (f : α → β → α) (a : α) (b : β) (l : list β) :

list.foldl f a (b :: l) = list.foldl f (f a b) l

source

@[simp]

theorem list.foldr_nil {α : Type u} {β : Type v} (f : α → β → β) (b : β) :

list.foldr f b list.nil = b

source

@[simp]

theorem list.foldr_cons {α : Type u} {β : Type v} (f : α → β → β) (b : β) (a : α) (l : list α) :

list.foldr f b (a :: l) = f a (list.foldr f b l)

source

@[simp]

theorem list.foldl_append {α : Type u} {β : Type v} (f : α → β → α) (a : α) (l₁ l₂ : list β) :

list.foldl f a (l₁ ++ l₂) = list.foldl f (list.foldl f a l₁) l₂

source

@[simp]

theorem list.foldr_append {α : Type u} {β : Type v} (f : α → β → β) (b : β) (l₁ l₂ : list α) :

list.foldr f b (l₁ ++ l₂) = list.foldr f (list.foldr f b l₂) l₁

source

@[simp]

theorem list.foldl_join {α : Type u} {β : Type v} (f : α → β → α) (a : α) (L : list (list β)) :

list.foldl f a L.join = list.foldl (list.foldl f) a L

source

@[simp]

theorem list.foldr_join {α : Type u} {β : Type v} (f : α → β → β) (b : β) (L : list (list α)) :

list.foldr f b L.join = list.foldr (λ (l : list α) (b : β), list.foldr f b l) b L

source

theorem list.foldl_reverse {α : Type u} {β : Type v} (f : α → β → α) (a : α) (l : list β) :

list.foldl f a l.reverse = list.foldr (λ (x : β) (y : α), f y x) a l

source

theorem list.foldr_reverse {α : Type u} {β : Type v} (f : α → β → β) (a : β) (l : list α) :

list.foldr f a l.reverse = list.foldl (λ (x : β) (y : α), f y x) a l

source

@[simp]

theorem list.foldr_eta {α : Type u} (l : list α) :

list.foldr list.cons list.nil l = l

source

@[simp]

theorem list.reverse_foldl {α : Type u} {l : list α} :

(list.foldl (λ (t : list α) (h : α), h :: t) list.nil l).reverse = l

source

@[simp]

theorem list.foldl_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → γ → α) (a : α) (l : list β) :

list.foldl f a (list.map g l) = list.foldl (λ (x : α) (y : β), f x (g y)) a l

source

@[simp]

theorem list.foldr_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : γ → α → α) (a : α) (l : list β) :

list.foldr f a (list.map g l) = list.foldr (f ∘ g) a l

source

theorem list.foldl_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : list α) :

(∀ (x y : α), f' (g x) (g y) = g (f x y)) → list.foldl f' (g a) (list.map g l) = g (list.foldl f a l)

source

theorem list.foldr_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : list α) :

(∀ (x y : α), f' (g x) (g y) = g (f x y)) → list.foldr f' (g a) (list.map g l) = g (list.foldr f a l)

source

theorem list.foldl_hom {α : Type u} {β : Type v} {γ : Type w} (l : list γ) (f : α → β) (op : α → γ → α) (op' : β → γ → β) (a : α) :

(∀ (a : α) (x : γ), f (op a x) = op' (f a) x) → list.foldl op' (f a) l = f (list.foldl op a l)

source

theorem list.foldr_hom {α : Type u} {β : Type v} {γ : Type w} (l : list γ) (f : α → β) (op : γ → α → α) (op' : γ → β → β) (a : α) :

(∀ (x : γ) (a : α), f (op x a) = op' x (f a)) → list.foldr op' (f a) l = f (list.foldr op a l)

source

theorem list.injective_foldl_comp {α : Type u_1} {l : list (α → α)} {f : α → α} :

(∀ (f : α → α), f ∈ l → function.injective f) → function.injective f → function.injective (list.foldl function.comp f l)

source

theorem list.length_scanl {α : Type u} {β : Type u_1} {f : α → β → α} (a : α) (l : list β) :

(list.scanl f a l).length = l.length + 1

source

@[simp]

theorem list.scanr_nil {α : Type u} {β : Type v} (f : α → β → β) (b : β) :

list.scanr f b list.nil = [b]

source

@[simp]

theorem list.scanr_aux_cons {α : Type u} {β : Type v} (f : α → β → β) (b : β) (a : α) (l : list α) :

list.scanr_aux f b (a :: l) = (list.foldr f b (a :: l), list.scanr f b l)

source

@[simp]

theorem list.scanr_cons {α : Type u} {β : Type v} (f : α → β → β) (b : β) (a : α) (l : list α) :

list.scanr f b (a :: l) = list.foldr f b (a :: l) :: list.scanr f b l

source

theorem list.foldl1_eq_foldr1 {α : Type u} {f : α → α → α} (hassoc : associative f) (a b : α) (l : list α) :

list.foldl f a (l ++ [b]) = list.foldr f b (a :: l)

source

theorem list.foldl_eq_of_comm_of_assoc {α : Type u} {f : α → α → α} (hcomm : commutative f) (hassoc : associative f) (a b : α) (l : list α) :

list.foldl f a (b :: l) = f b (list.foldl f a l)

source

theorem list.foldl_eq_foldr {α : Type u} {f : α → α → α} (hcomm : commutative f) (hassoc : associative f) (a : α) (l : list α) :

list.foldl f a l = list.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 β) :

list.foldl f a (b :: l) = f (list.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 β) :

list.foldl f a l = list.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 α) :

list.foldr f a (b :: l) = list.foldr f (f b a) l

source

theorem list.foldl_assoc {α : Type u} {op : α → α → α} [ha : is_associative α op] {l : list α} {a₁ a₂ : α} :

list.foldl op (op a₁ a₂) l = op a₁ (list.foldl op a₂ l)

source

theorem list.foldl_op_eq_op_foldr_assoc {α : Type u} {op : α → α → α} [ha : is_associative α op] {l : list α} {a₁ a₂ : α} :

op (list.foldl op a₁ l) a₂ = op a₁ (list.foldr op a₂ l)

source

theorem list.foldl_assoc_comm_cons {α : Type u} {op : α → α → α} [ha : is_associative α op] [hc : is_commutative α op] {l : list α} {a₁ a₂ : α} :

list.foldl op a₂ (a₁ :: l) = op a₁ (list.foldl op a₂ l)

source

@[simp]

theorem list.mfoldl_nil {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] (f : β → α → m β) {b : β} :

list.mfoldl f b list.nil = has_pure.pure b

source

@[simp]

theorem list.mfoldr_nil {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] (f : α → β → m β) {b : β} :

list.mfoldr f b list.nil = has_pure.pure b

source

@[simp]

theorem list.mfoldl_cons {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] {f : β → α → m β} {b : β} {a : α} {l : list α} :

list.mfoldl f b (a :: l) = f b a >>= λ (b' : β), list.mfoldl f b' l

source

@[simp]

theorem list.mfoldr_cons {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] {f : α → β → m β} {b : β} {a : α} {l : list α} :

list.mfoldr f b (a :: l) = list.mfoldr f b l >>= f a

source

theorem list.mfoldr_eq_foldr {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] (f : α → β → m β) (b : β) (l : list α) :

list.mfoldr f b l = list.foldr (λ (a : α) (mb : m β), mb >>= f a) (has_pure.pure b) l

source

theorem list.mfoldl_eq_foldl {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] [is_lawful_monad m] (f : β → α → m β) (b : β) (l : list α) :

list.mfoldl f b l = list.foldl (λ (mb : m β) (a : α), mb >>= λ (b : β), f b a) (has_pure.pure b) l

source

@[simp]

theorem list.mfoldl_append {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] [is_lawful_monad m] {f : β → α → m β} {b : β} {l₁ l₂ : list α} :

list.mfoldl f b (l₁ ++ l₂) = list.mfoldl f b l₁ >>= λ (x : β), list.mfoldl f x l₂

source

@[simp]

theorem list.mfoldr_append {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] [is_lawful_monad m] {f : α → β → m β} {b : β} {l₁ l₂ : list α} :

list.mfoldr f b (l₁ ++ l₂) = list.mfoldr f b l₂ >>= λ (x : β), list.mfoldr f x l₁

source

@[simp]

theorem list.prod_nil {α : Type u} [monoid α] :

list.nil.prod = 1

source

@[simp]

theorem list.sum_nil {α : Type u} [add_monoid α] :

list.nil.sum = 0

source

theorem list.sum_singleton {α : Type u} [add_monoid α] {a : α} :

[a].sum = a

source

theorem list.prod_singleton {α : Type u} [monoid α] {a : α} :

[a].prod = a

source

@[simp]

theorem list.prod_cons {α : Type u} [monoid α] {l : list α} {a : α} :

(a :: l).prod = a * l.prod

source

@[simp]

theorem list.sum_cons {α : Type u} [add_monoid α] {l : list α} {a : α} :

(a :: l).sum = a + l.sum

source

@[simp]

theorem list.prod_append {α : Type u} [monoid α] {l₁ l₂ : list α} :

(l₁ ++ l₂).prod = l₁.prod * l₂.prod

source

@[simp]

theorem list.sum_append {α : Type u} [add_monoid α] {l₁ l₂ : list α} :

(l₁ ++ l₂).sum = l₁.sum + l₂.sum

source

@[simp]

theorem list.prod_join {α : Type u} [monoid α] {l : list (list α)} :

l.join.prod = (list.map list.prod l).prod

source

@[simp]

theorem list.sum_join {α : Type u} [add_monoid α] {l : list (list α)} :

l.join.sum = (list.map list.sum l).sum

source

theorem list.prod_ne_zero {R : Type u_1} [domain R] {L : list R} :

(∀ (x : R), x ∈ L → x ≠ 0) → L.prod ≠ 0

source

theorem list.prod_eq_foldr {α : Type u} [monoid α] {l : list α} :

l.prod = list.foldr has_mul.mul 1 l

source

theorem list.sum_eq_foldr {α : Type u} [add_monoid α] {l : list α} :

l.sum = list.foldr has_add.add 0 l

source

theorem list.prod_hom_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [monoid β] [monoid γ] (l : list α) {r : β → γ → Prop} {f : α → β} {g : α → γ} :

r 1 1 → (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b c → r (f a * b) (g a * c)) → r (list.map f l).prod (list.map g l).prod

source

theorem list.sum_hom_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_monoid β] [add_monoid γ] (l : list α) {r : β → γ → Prop} {f : α → β} {g : α → γ} :

r 0 0 → (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b c → r (f a + b) (g a + c)) → r (list.map f l).sum (list.map g l).sum

source

theorem list.sum_hom {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] (l : list α) (f : α → β) [is_add_monoid_hom f] :

(list.map f l).sum = f l.sum

source

theorem list.prod_hom {α : Type u} {β : Type v} [monoid α] [monoid β] (l : list α) (f : α → β) [is_monoid_hom f] :

(list.map f l).prod = f l.prod

source

@[simp]

theorem list.prod_take_mul_prod_drop {α : Type u} [monoid α] (L : list α) (i : ℕ) :

(list.take i L).prod * (list.drop i L).prod = L.prod

source

@[simp]

theorem list.prod_take_succ {α : Type u} [monoid α] (L : list α) (i : ℕ) (p : i < L.length) :

(list.take (i + 1) L).prod = (list.take i L).prod * L.nth_le i p

source

theorem list.length_pos_of_prod_ne_one {α : Type u} [monoid α] (L : list α) :

L.prod ≠ 1 → 0 < L.length

A list with product not one must have positive length.

source

@[simp]

theorem list.sum_take_add_sum_drop {α : Type u} [add_monoid α] (L : list α) (i : ℕ) :

(list.take i L).sum + (list.drop i L).sum = L.sum

source

@[simp]

theorem list.sum_take_succ {α : Type u} [add_monoid α] (L : list α) (i : ℕ) (p : i < L.length) :

(list.take (i + 1) L).sum = (list.take i L).sum + L.nth_le i p

source

theorem list.eq_of_sum_take_eq {α : Type u} [add_left_cancel_monoid α] {L L' : list α} :

L.length = L'.length → (∀ (i : ℕ), i ≤ L.length → (list.take i L).sum = (list.take i L').sum) → L = L'

source

theorem list.monotone_sum_take {α : Type u} [canonically_ordered_add_monoid α] (L : list α) :

monotone (λ (i : ℕ), (list.take i L).sum)

source

theorem list.length_pos_of_sum_ne_zero {α : Type u} [add_monoid α] (L : list α) :

L.sum ≠ 0 → 0 < L.length

A list with sum not zero must have positive length.

source

theorem list.length_le_sum_of_one_le (L : list ℕ) :

(∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum

If all elements in a list are bounded below by 1, then the length of the list is bounded by the sum of the elements.

source

theorem list.length_pos_of_sum_pos {α : Type u} [ordered_cancel_add_comm_monoid α] (L : list α) :

0 < L.sum → 0 < L.length

A list with positive sum must have positive length.

source

@[simp]

theorem list.sum_erase {α : Type u} [decidable_eq α] [add_comm_monoid α] {a : α} {l : list α} :

a ∈ l → a + (l.erase a).sum = l.sum

source

@[simp]

theorem list.prod_erase {α : Type u} [decidable_eq α] [comm_monoid α] {a : α} {l : list α} :

a ∈ l → a * (l.erase a).prod = l.prod

source

theorem list.dvd_prod {α : Type u} [comm_semiring α] {a : α} {l : list α} :

a ∈ l → a ∣ l.prod

source

@[simp]

theorem list.sum_const_nat (m n : ℕ) :

(list.repeat m n).sum = m * n

source

theorem list.dvd_sum {α : Type u} [comm_semiring α] {a : α} {l : list α} :

(∀ (x : α), x ∈ l → a ∣ x) → a ∣ l.sum

source

@[simp]

theorem list.length_join {α : Type u} (L : list (list α)) :

L.join.length = (list.map list.length L).sum

source

@[simp]

theorem list.length_bind {α : Type u} {β : Type v} (l : list α) (f : α → list β) :

(l.bind f).length = (list.map (list.length ∘ f) l).sum

source

theorem list.exists_lt_of_sum_lt {α : Type u} {β : Type v} [decidable_linear_ordered_cancel_add_comm_monoid β] {l : list α} (f g : α → β) :

(list.map f l).sum < (list.map g l).sum → (∃ (x : α) (H : x ∈ l), f x < g x)

source

theorem list.exists_le_of_sum_le {α : Type u} {β : Type v} [decidable_linear_ordered_cancel_add_comm_monoid β] {l : list α} (hl : l ≠ list.nil) (f g : α → β) :

(list.map f l).sum ≤ (list.map g l).sum → (∃ (x : α) (H : x ∈ l), f x ≤ g x)

source

theorem list.head_mul_tail_prod' {α : Type u} [monoid α] (L : list α) :

(L.nth 0).get_or_else 1 * L.tail.prod = L.prod

source

theorem list.head_add_tail_sum' {α : Type u} [add_monoid α] (L : list α) :

(L.nth 0).get_or_else 0 + L.tail.sum = L.sum

source

theorem list.head_add_tail_sum (L : list ℕ) :

L.head + L.tail.sum = L.sum

source

theorem list.head_le_sum (L : list ℕ) :

L.head ≤ L.sum

source

theorem list.tail_sum (L : list ℕ) :

L.tail.sum = L.sum - L.head

source

@[simp]

theorem list.alternating_prod_nil {G : Type u_1} [comm_group G] :

list.nil.alternating_prod = 1

source

@[simp]

theorem list.alternating_sum_nil {G : Type u_1} [add_comm_group G] :

list.nil.alternating_sum = 0

source

@[simp]

theorem list.alternating_prod_singleton {G : Type u_1} [comm_group G] (g : G) :

[g].alternating_prod = g

source

@[simp]

theorem list.alternating_sum_singleton {G : Type u_1} [add_comm_group G] (g : G) :

[g].alternating_sum = g

source

@[simp]

theorem list.alternating_sum_cons_cons' {G : Type u_1} [add_comm_group G] (g h : G) (l : list G) :

(g :: h :: l).alternating_sum = g + -h + l.alternating_sum

source

@[simp]

theorem list.alternating_prod_cons_cons {G : Type u_1} [comm_group G] (g h : G) (l : list G) :

(g :: h :: l).alternating_prod = g * h⁻¹ * l.alternating_prod

source

theorem list.alternating_sum_cons_cons {G : Type u_1} [add_comm_group G] (g h : G) (l : list G) :

(g :: h :: l).alternating_sum = g - h + l.alternating_sum

source

theorem list.join_eq_nil {α : Type u} {L : list (list α)} :

L.join = list.nil ↔ ∀ (l : list α), l ∈ L → l = list.nil

source

@[simp]

theorem list.join_append {α : Type u} (L₁ L₂ : list (list α)) :

(L₁ ++ L₂).join = L₁.join ++ L₂.join

source

theorem list.join_join {α : Type u} (l : list (list (list α))) :

l.join.join = (list.map list.join l).join

source

theorem list.take_sum_join {α : Type u} (L : list (list α)) (i : ℕ) :

list.take (list.take i (list.map list.length L)).sum L.join = (list.take i L).join

In a join, taking the first elements up to an index which is the sum of the lengths of the first i sublists, is the same as taking the join of the first i sublists.

source

theorem list.drop_sum_join {α : Type u} (L : list (list α)) (i : ℕ) :

list.drop (list.take i (list.map list.length L)).sum L.join = (list.drop i L).join

In a join, dropping all the elements up to an index which is the sum of the lengths of the first i sublists, is the same as taking the join after dropping the first i sublists.

source

theorem list.drop_take_succ_eq_cons_nth_le {α : Type u} (L : list α) {i : ℕ} (hi : i < L.length) :

list.drop i (list.take (i + 1) L) = [L.nth_le i hi]

Taking only the first i+1 elements in a list, and then dropping the first i ones, one is left with a list of length 1 made of the i-th element of the original list.

source

theorem list.drop_take_succ_join_eq_nth_le {α : Type u} (L : list (list α)) {i : ℕ} (hi : i < L.length) :

list.drop (list.take i (list.map list.length L)).sum (list.take (list.take (i + 1) (list.map list.length L)).sum L.join) = L.nth_le i hi

In a join of sublists, taking the slice between the indices A and B - 1 gives back the original sublist of index i if A is the sum of the lenghts of sublists of index < i, and B is the sum of the lengths of sublists of index ≤ i.

source

theorem list.sum_take_map_length_lt1 {α : Type u} (L : list (list α)) {i j : ℕ} (hi : i < L.length) :

j < (L.nth_le i hi).length → (list.take i (list.map list.length L)).sum + j < (list.take (i + 1) (list.map list.length L)).sum

Auxiliary lemma to control elements in a join.

source

theorem list.sum_take_map_length_lt2 {α : Type u} (L : list (list α)) {i j : ℕ} (hi : i < L.length) :

j < (L.nth_le i hi).length → (list.take i (list.map list.length L)).sum + j < L.join.length

Auxiliary lemma to control elements in a join.

source

theorem list.nth_le_join {α : Type u} (L : list (list α)) {i j : ℕ} (hi : i < L.length) (hj : j < (L.nth_le i hi).length) :

L.join.nth_le ((list.take i (list.map list.length L)).sum + j) _ = (L.nth_le i hi).nth_le j hj

The n-th element in a join of sublists is the j-th element of the ith sublist, where n can be obtained in terms of i and j by adding the lengths of all the sublists of index < i, and adding j.

source

theorem list.eq_iff_join_eq {α : Type u} (L L' : list (list α)) :

L = L' ↔ L.join = L'.join ∧ list.map list.length L = list.map list.length L'

Two lists of sublists are equal iff their joins coincide, as well as the lengths of the sublists.

source

inductive list.lex {α : Type u} :

(α → α → Prop) → list α → list α → Prop

nil : ∀ {α : Type u} (r : α → α → Prop) {a : α} {l : list α}, list.lex r list.nil (a :: l)
cons : ∀ {α : Type u} (r : α → α → Prop) {a : α} {l₁ l₂ : list α}, list.lex r l₁ l₂ → list.lex r (a :: l₁) (a :: l₂)
rel : ∀ {α : Type u} (r : α → α → Prop) {a₁ : α} {l₁ : list α} {a₂ : α} {l₂ : list α}, r a₁ a₂ → list.lex r (a₁ :: l₁) (a₂ :: l₂)

Given a strict order < on α, the lexicographic strict order on list α, for which [a0, ..., an] < [b0, ..., b_k] if a0 < b0 or a0 = b0 and [a1, ..., an] < [b1, ..., bk]. The definition is given for any relation r, not only strict orders.

source

theorem list.lex.cons_iff {α : Type u} {r : α → α → Prop} [is_irrefl α r] {a : α} {l₁ l₂ : list α} :

list.lex r (a :: l₁) (a :: l₂) ↔ list.lex r l₁ l₂

source

@[simp]

theorem list.lex.not_nil_right {α : Type u} (r : α → α → Prop) (l : list α) :

¬list.lex r l list.nil

source

@[instance]

def list.lex.is_order_connected {α : Type u} (r : α → α → Prop) [is_order_connected α r] [is_trichotomous α r] :

is_order_connected (list α) (list.lex r)

Equations

_ = _
_ = _
_ = _
_ = _
_ = _
_ = _
_ = _

source

@[instance]

def list.lex.is_trichotomous {α : Type u} (r : α → α → Prop) [is_trichotomous α r] :

is_trichotomous (list α) (list.lex r)

Equations

_ = _
_ = _
_ = _
_ = _
_ = _

source

@[instance]

def list.lex.is_asymm {α : Type u} (r : α → α → Prop) [is_asymm α r] :

is_asymm (list α) (list.lex r)

Equations

_ = _
_ = _
_ = _
_ = _
_ = _

source

@[instance]

def list.lex.is_strict_total_order {α : Type u} (r : α → α → Prop) [is_strict_total_order' α r] :

is_strict_total_order' (list α) (list.lex r)

Equations

_ = is_strict_total_order'.mk

source

@[instance]

def list.lex.decidable_rel {α : Type u} [decidable_eq α] (r : α → α → Prop) [decidable_rel r] :

decidable_rel (list.lex r)

Equations

list.lex.decidable_rel r (a :: l₁) (b :: l₂) = decidable_of_iff (r a b ∨ a = b ∧ list.lex r l₁ l₂) _
list.lex.decidable_rel r (hd :: tl) list.nil = decidable.is_false _
list.lex.decidable_rel r list.nil (b :: l₂) = decidable.is_true list.lex.nil
list.lex.decidable_rel r list.nil list.nil = decidable.is_false _

source

theorem list.lex.append_right {α : Type u} (r : α → α → Prop) {s₁ s₂ : list α} (t : list α) :

list.lex r s₁ s₂ → list.lex r s₁ (s₂ ++ t)

source

theorem list.lex.append_left {α : Type u} (R : α → α → Prop) {t₁ t₂ : list α} (h : list.lex R t₁ t₂) (s : list α) :

list.lex R (s ++ t₁) (s ++ t₂)

source

theorem list.lex.imp {α : Type u} {r s : α → α → Prop} (H : ∀ (a b : α), r a b → s a b) (l₁ l₂ : list α) :

list.lex r l₁ l₂ → list.lex s l₁ l₂

source

theorem list.lex.to_ne {α : Type u} {l₁ l₂ : list α} :

list.lex ne l₁ l₂ → l₁ ≠ l₂

source

theorem list.lex.ne_iff {α : Type u} {l₁ l₂ : list α} :

l₁.length ≤ l₂.length → (list.lex ne l₁ l₂ ↔ l₁ ≠ l₂)

source

@[instance]

def list.has_lt' {α : Type u} [has_lt α] :

has_lt (list α)

Equations

list.has_lt' = {lt := list.lex has_lt.lt}

source

theorem list.nil_lt_cons {α : Type u} [has_lt α] (a : α) (l : list α) :

list.nil < a :: l

source

@[instance]

def list.linear_order {α : Type u} [linear_order α] :

linear_order (list α)

Equations

list.linear_order = linear_order_of_STO' (list.lex has_lt.lt)

source

@[instance]

def list.has_le' {α : Type u} [linear_order α] :

has_le (list α)

Equations

list.has_le' = preorder.to_has_le (list α)

source

@[instance]

def list.decidable_linear_order {α : Type u} [decidable_linear_order α] :

decidable_linear_order (list α)

Equations

list.decidable_linear_order = decidable_linear_order_of_STO' (list.lex has_lt.lt)

source

@[simp]

theorem list.all_nil {α : Type u} (p : α → bool) :

list.nil.all p = bool.tt

source

@[simp]

theorem list.all_cons {α : Type u} (p : α → bool) (a : α) (l : list α) :

(a :: l).all p = p a && l.all p

source

theorem list.all_iff_forall {α : Type u} {p : α → bool} {l : list α} :

↥(l.all p) ↔ ∀ (a : α), a ∈ l → ↥(p a)

source

theorem list.all_iff_forall_prop {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :

↥(l.all (λ (a : α), decidable.to_bool (p a))) ↔ ∀ (a : α), a ∈ l → p a

source

@[simp]

theorem list.any_nil {α : Type u} (p : α → bool) :

list.nil.any p = bool.ff

source

@[simp]

theorem list.any_cons {α : Type u} (p : α → bool) (a : α) (l : list α) :

(a :: l).any p = p a || l.any p

source

theorem list.any_iff_exists {α : Type u} {p : α → bool} {l : list α} :

↥(l.any p) ↔ ∃ (a : α) (H : a ∈ l), ↥(p a)

source

theorem list.any_iff_exists_prop {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :

↥(l.any (λ (a : α), decidable.to_bool (p a))) ↔ ∃ (a : α) (H : a ∈ l), p a

source

theorem list.any_of_mem {α : Type u} {p : α → bool} {a : α} {l : list α} :

a ∈ l → ↥(p a) → ↥(l.any p)

source

@[instance]

def list.decidable_forall_mem {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :

decidable (∀ (x : α), x ∈ l → p x)

Equations

l.decidable_forall_mem = decidable_of_iff ↥(l.all (λ (a : α), decidable.to_bool (p a))) _

source

@[instance]

def list.decidable_exists_mem {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :

decidable (∃ (x : α) (H : x ∈ l), p x)

Equations

l.decidable_exists_mem = decidable_of_iff ↥(l.any (λ (a : α), decidable.to_bool (p a))) _

source

@[simp]

def list.pmap {α : Type u} {β : Type v} {p : α → Prop} (f : Π (a : α), p a → β) (l : list α) :

(∀ (a : α), a ∈ l → p a) → list β

Partial map. If f : Π a, p a → β is a partial function defined on a : α satisfying p, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy p, using the proof to apply f.

Equations

list.pmap f (a :: l) H = f a _ :: list.pmap f l _
list.pmap f list.nil H = list.nil

source

def list.attach {α : Type u} (l : list α) :

list {x // x ∈ l}

"Attach" the proof that the elements of l are in l to produce a new list with the same elements but in the type {x // x ∈ l}.

Equations

l.attach = list.pmap subtype.mk l _

source

theorem list.sizeof_lt_sizeof_of_mem {α : Type u} [has_sizeof α] {x : α} {l : list α} :

x ∈ l → sizeof x < sizeof l

source

theorem list.pmap_eq_map {α : Type u} {β : Type v} (p : α → Prop) (f : α → β) (l : list α) (H : ∀ (a : α), a ∈ l → p a) :

list.pmap (λ (a : α) (_x : p a), f a) l H = list.map f l

source

theorem list.pmap_congr {α : Type u} {β : Type v} {p q : α → Prop} {f : Π (a : α), p a → β} {g : Π (a : α), q a → β} (l : list α) {H₁ : ∀ (a : α), a ∈ l → p a} {H₂ : ∀ (a : α), a ∈ l → q a} :

(∀ (a : α) (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → list.pmap f l H₁ = list.pmap g l H₂

source

theorem list.map_pmap {α : Type u} {β : Type v} {γ : Type w} {p : α → Prop} (g : β → γ) (f : Π (a : α), p a → β) (l : list α) (H : ∀ (a : α), a ∈ l → p a) :

list.map g (list.pmap f l H) = list.pmap (λ (a : α) (h : p a), g (f a h)) l H

source

theorem list.pmap_eq_map_attach {α : Type u} {β : Type v} {p : α → Prop} (f : Π (a : α), p a → β) (l : list α) (H : ∀ (a : α), a ∈ l → p a) :

list.pmap f l H = list.map (λ (x : {x // x ∈ l}), f x.val _) l.attach

source

theorem list.attach_map_val {α : Type u} (l : list α) :

list.map subtype.val l.attach = l

source

@[simp]

theorem list.mem_attach {α : Type u} (l : list α) (x : {x // x ∈ l}) :

x ∈ l.attach

source

@[simp]

theorem list.mem_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : Π (a : α), p a → β} {l : list α} {H : ∀ (a : α), a ∈ l → p a} {b : β} :

b ∈ list.pmap f l H ↔ ∃ (a : α) (h : a ∈ l), f a _ = b

source

@[simp]

theorem list.length_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : Π (a : α), p a → β} {l : list α} {H : ∀ (a : α), a ∈ l → p a} :

(list.pmap f l H).length = l.length

source

@[simp]

theorem list.length_attach {α : Type u} (L : list α) :

L.attach.length = L.length

source

@[simp]

theorem list.find_nil {α : Type u} (p : α → Prop) [decidable_pred p] :

list.find p list.nil = option.none

source

@[simp]

theorem list.find_cons_of_pos {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (l : list α) :

p a → list.find p (a :: l) = option.some a

source

@[simp]

theorem list.find_cons_of_neg {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (l : list α) :

¬p a → list.find p (a :: l) = list.find p l

source

@[simp]

theorem list.find_eq_none {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :

list.find p l = option.none ↔ ∀ (x : α), x ∈ l → ¬p x

source

theorem list.find_some {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} :

list.find p l = option.some a → p a

source

@[simp]

theorem list.find_mem {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} :

list.find p l = option.some a → a ∈ l

source

@[simp]

theorem list.lookmap_nil {α : Type u} (f : α → option α) :

list.lookmap f list.nil = list.nil

source

@[simp]

theorem list.lookmap_cons_none {α : Type u} (f : α → option α) {a : α} (l : list α) :

f a = option.none → list.lookmap f (a :: l) = a :: list.lookmap f l

source

@[simp]

theorem list.lookmap_cons_some {α : Type u} (f : α → option α) {a b : α} (l : list α) :

f a = option.some b → list.lookmap f (a :: l) = b :: l

source

theorem list.lookmap_some {α : Type u} (l : list α) :

list.lookmap option.some l = l

source

theorem list.lookmap_none {α : Type u} (l : list α) :

list.lookmap (λ (_x : α), option.none) l = l

source

theorem list.lookmap_congr {α : Type u} {f g : α → option α} {l : list α} :

(∀ (a : α), a ∈ l → f a = g a) → list.lookmap f l = list.lookmap g l

source

theorem list.lookmap_of_forall_not {α : Type u} (f : α → option α) {l : list α} :

(∀ (a : α), a ∈ l → f a = option.none) → list.lookmap f l = l

source

theorem list.lookmap_map_eq {α : Type u} {β : Type v} (f : α → option α) (g : α → β) (h : ∀ (a b : α), b ∈ f a → g a = g b) (l : list α) :

list.map g (list.lookmap f l) = list.map g l

source

theorem list.lookmap_id' {α : Type u} (f : α → option α) (h : ∀ (a b : α), b ∈ f a → a = b) (l : list α) :

list.lookmap f l = l

source

theorem list.length_lookmap {α : Type u} (f : α → option α) (l : list α) :

(list.lookmap f l).length = l.length

source

@[simp]

theorem list.filter_map_nil {α : Type u} {β : Type v} (f : α → option β) :

list.filter_map f list.nil = list.nil

source

@[simp]

theorem list.filter_map_cons_none {α : Type u} {β : Type v} {f : α → option β} (a : α) (l : list α) :

f a = option.none → list.filter_map f (a :: l) = list.filter_map f l

source

@[simp]

theorem list.filter_map_cons_some {α : Type u} {β : Type v} (f : α → option β) (a : α) (l : list α) {b : β} :

f a = option.some b → list.filter_map f (a :: l) = b :: list.filter_map f l

source

theorem list.filter_map_eq_map {α : Type u} {β : Type v} (f : α → β) :

list.filter_map (option.some ∘ f) = list.map f

source

theorem list.filter_map_eq_filter {α : Type u} (p : α → Prop) [decidable_pred p] :

list.filter_map (option.guard p) = list.filter p

source

theorem list.filter_map_filter_map {α : Type u} {β : Type v} {γ : Type w} (f : α → option β) (g : β → option γ) (l : list α) :

list.filter_map g (list.filter_map f l) = list.filter_map (λ (x : α), (f x).bind g) l

source

theorem list.map_filter_map {α : Type u} {β : Type v} {γ : Type w} (f : α → option β) (g : β → γ) (l : list α) :

list.map g (list.filter_map f l) = list.filter_map (λ (x : α), option.map g (f x)) l

source

theorem list.filter_map_map {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → option γ) (l : list α) :

list.filter_map g (list.map f l) = list.filter_map (g ∘ f) l

source

theorem list.filter_filter_map {α : Type u} {β : Type v} (f : α → option β) (p : β → Prop) [decidable_pred p] (l : list α) :

list.filter p (list.filter_map f l) = list.filter_map (λ (x : α), option.filter p (f x)) l

source

theorem list.filter_map_filter {α : Type u} {β : Type v} (p : α → Prop) [decidable_pred p] (f : α → option β) (l : list α) :

list.filter_map f (list.filter p l) = list.filter_map (λ (x : α), ite (p x) (f x) option.none) l

source

@[simp]

theorem list.filter_map_some {α : Type u} (l : list α) :

list.filter_map option.some l = l

source

@[simp]

theorem list.mem_filter_map {α : Type u} {β : Type v} (f : α → option β) (l : list α) {b : β} :

b ∈ list.filter_map f l ↔ ∃ (a : α), a ∈ l ∧ f a = option.some b

source

theorem list.map_filter_map_of_inv {α : Type u} {β : Type v} (f : α → option β) (g : β → α) (H : ∀ (x : α), option.map g (f x) = option.some x) (l : list α) :

list.map g (list.filter_map f l) = l

source

theorem list.sublist.filter_map {α : Type u} {β : Type v} (f : α → option β) {l₁ l₂ : list α} :

l₁ <+ l₂ → list.filter_map f l₁ <+ list.filter_map f l₂

source

theorem list.sublist.map {α : Type u} {β : Type v} (f : α → β) {l₁ l₂ : list α} :

l₁ <+ l₂ → list.map f l₁ <+ list.map f l₂

source

theorem list.filter_eq_foldr {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :

list.filter p l = list.foldr (λ (a : α) (out : list α), ite (p a) (a :: out) out) list.nil l

source

theorem list.filter_congr {α : Type u} {p q : α → Prop} [decidable_pred p] [decidable_pred q] {l : list α} :

(∀ (x : α), x ∈ l → (p x ↔ q x)) → list.filter p l = list.filter q l

source

@[simp]

theorem list.filter_subset {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :

list.filter p l ⊆ l

source

theorem list.of_mem_filter {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

a ∈ list.filter p l → p a

source

theorem list.mem_of_mem_filter {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

a ∈ list.filter p l → a ∈ l

source

theorem list.mem_filter_of_mem {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

a ∈ l → p a → a ∈ list.filter p l

source

@[simp]

theorem list.mem_filter {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

a ∈ list.filter p l ↔ a ∈ l ∧ p a

source

theorem list.filter_eq_self {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :

list.filter p l = l ↔ ∀ (a : α), a ∈ l → p a

source

theorem list.filter_eq_nil {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :

list.filter p l = list.nil ↔ ∀ (a : α), a ∈ l → ¬p a

source

theorem list.filter_sublist_filter {α : Type u} {p : α → Prop} [decidable_pred p] {l₁ l₂ : list α} :

l₁ <+ l₂ → list.filter p l₁ <+ list.filter p l₂

source

theorem list.filter_of_map {α : Type u} {β : Type v} {p : α → Prop} [decidable_pred p] (f : β → α) (l : list β) :

list.filter p (list.map f l) = list.map f (list.filter (p ∘ f) l)

source

@[simp]

theorem list.filter_filter {α : Type u} {p : α → Prop} [decidable_pred p] {q : α → Prop} [decidable_pred q] (l : list α) :

list.filter p (list.filter q l) = list.filter (λ (a : α), p a ∧ q a) l

source

@[simp]

theorem list.filter_true {α : Type u} {h : decidable_pred (λ (a : α), true)} (l : list α) :

list.filter (λ (_x : α), true) l = l

source

@[simp]

theorem list.filter_false {α : Type u} {h : decidable_pred (λ (a : α), false)} (l : list α) :

list.filter (λ (_x : α), false) l = list.nil

source

@[simp]

theorem list.span_eq_take_drop {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :

list.span p l = (list.take_while p l, list.drop_while p l)

source

@[simp]

theorem list.take_while_append_drop {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :

list.take_while p l ++ list.drop_while p l = l

source

@[simp]

theorem list.countp_nil {α : Type u} (p : α → Prop) [decidable_pred p] :

list.countp p list.nil = 0

source

@[simp]

theorem list.countp_cons_of_pos {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (l : list α) :

p a → list.countp p (a :: l) = list.countp p l + 1

source

@[simp]

theorem list.countp_cons_of_neg {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (l : list α) :

¬p a → list.countp p (a :: l) = list.countp p l

source

theorem list.countp_eq_length_filter {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :

list.countp p l = (list.filter p l).length

source

@[simp]

theorem list.countp_append {α : Type u} {p : α → Prop} [decidable_pred p] (l₁ l₂ : list α) :

list.countp p (l₁ ++ l₂) = list.countp p l₁ + list.countp p l₂

source

theorem list.countp_pos {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :

0 < list.countp p l ↔ ∃ (a : α) (H : a ∈ l), p a

source

theorem list.countp_le_of_sublist {α : Type u} {p : α → Prop} [decidable_pred p] {l₁ l₂ : list α} :

l₁ <+ l₂ → list.countp p l₁ ≤ list.countp p l₂

source

@[simp]

theorem list.countp_filter {α : Type u} {p : α → Prop} [decidable_pred p] {q : α → Prop} [decidable_pred q] (l : list α) :

list.countp p (list.filter q l) = list.countp (λ (a : α), p a ∧ q a) l

source

@[simp]

theorem list.count_nil {α : Type u} [decidable_eq α] (a : α) :

list.count a list.nil = 0

source

theorem list.count_cons {α : Type u} [decidable_eq α] (a b : α) (l : list α) :

list.count a (b :: l) = ite (a = b) (list.count a l).succ (list.count a l)

source

theorem list.count_cons' {α : Type u} [decidable_eq α] (a b : α) (l : list α) :

list.count a (b :: l) = list.count a l + ite (a = b) 1 0

source

@[simp]

theorem list.count_cons_self {α : Type u} [decidable_eq α] (a : α) (l : list α) :

list.count a (a :: l) = (list.count a l).succ

source

@[simp]

theorem list.count_cons_of_ne {α : Type u} [decidable_eq α] {a b : α} (h : a ≠ b) (l : list α) :

list.count a (b :: l) = list.count a l

source

theorem list.count_tail {α : Type u} [decidable_eq α] (l : list α) (a : α) (h : 0 < l.length) :

list.count a l.tail = list.count a l - ite (a = l.nth_le 0 h) 1 0

source

theorem list.count_le_of_sublist {α : Type u} [decidable_eq α] (a : α) {l₁ l₂ : list α} :

l₁ <+ l₂ → list.count a l₁ ≤ list.count a l₂

source

theorem list.count_le_count_cons {α : Type u} [decidable_eq α] (a b : α) (l : list α) :

list.count a l ≤ list.count a (b :: l)

source

theorem list.count_singleton {α : Type u} [decidable_eq α] (a : α) :

list.count a [a] = 1

source

@[simp]

theorem list.count_append {α : Type u} [decidable_eq α] (a : α) (l₁ l₂ : list α) :

list.count a (l₁ ++ l₂) = list.count a l₁ + list.count a l₂

source

theorem list.count_concat {α : Type u} [decidable_eq α] (a : α) (l : list α) :

list.count a (l.concat a) = (list.count a l).succ

source

theorem list.count_pos {α : Type u} [decidable_eq α] {a : α} {l : list α} :

0 < list.count a l ↔ a ∈ l

source

@[simp]

theorem list.count_eq_zero_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∉ l → list.count a l = 0

source

theorem list.not_mem_of_count_eq_zero {α : Type u} [decidable_eq α] {a : α} {l : list α} :

list.count a l = 0 → a ∉ l

source

@[simp]

theorem list.count_repeat {α : Type u} [decidable_eq α] (a : α) (n : ℕ) :

list.count a (list.repeat a n) = n

source

theorem list.le_count_iff_repeat_sublist {α : Type u} [decidable_eq α] {a : α} {l : list α} {n : ℕ} :

n ≤ list.count a l ↔ list.repeat a n <+ l

source

theorem list.repeat_count_eq_of_count_eq_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :

list.count a l = l.length → list.repeat a (list.count a l) = l

source

@[simp]

theorem list.count_filter {α : Type u} [decidable_eq α] {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

p a → list.count a (list.filter p l) = list.count a l

source

@[simp]

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

l₁ <+: l₁ ++ l₂

source

@[simp]

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

l₂ <:+ l₁ ++ l₂

source

theorem list.infix_append {α : Type u} (l₁ l₂ l₃ : list α) :

l₂ <:+: l₁ ++ l₂ ++ l₃

source

@[simp]

theorem list.infix_append' {α : Type u} (l₁ l₂ l₃ : list α) :

l₂ <:+: l₁ ++ (l₂ ++ l₃)

source

theorem list.nil_prefix {α : Type u} (l : list α) :

list.nil <+: l

source

theorem list.nil_suffix {α : Type u} (l : list α) :

list.nil <:+ l

source

theorem list.prefix_refl {α : Type u} (l : list α) :

l <+: l

source

theorem list.suffix_refl {α : Type u} (l : list α) :

l <:+ l

source

@[simp]

theorem list.suffix_cons {α : Type u} (a : α) (l : list α) :

l <:+ a :: l

source

theorem list.prefix_concat {α : Type u} (a : α) (l : list α) :

l <+: l.concat a

source

theorem list.infix_of_prefix {α : Type u} {l₁ l₂ : list α} :

l₁ <+: l₂ → l₁ <:+: l₂

source

theorem list.infix_of_suffix {α : Type u} {l₁ l₂ : list α} :

l₁ <:+ l₂ → l₁ <:+: l₂

source

theorem list.infix_refl {α : Type u} (l : list α) :

l <:+: l

source

theorem list.nil_infix {α : Type u} (l : list α) :

list.nil <:+: l

source

theorem list.infix_cons {α : Type u} {L₁ L₂ : list α} {x : α} :

L₁ <:+: L₂ → L₁ <:+: x :: L₂

source

theorem list.is_prefix.trans {α : Type u} {l₁ l₂ l₃ : list α} :

l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃

source

theorem list.is_suffix.trans {α : Type u} {l₁ l₂ l₃ : list α} :

l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃

source

theorem list.is_infix.trans {α : Type u} {l₁ l₂ l₃ : list α} :

l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃

source

theorem list.sublist_of_infix {α : Type u} {l₁ l₂ : list α} :

l₁ <:+: l₂ → l₁ <+ l₂

source

theorem list.sublist_of_prefix {α : Type u} {l₁ l₂ : list α} :

l₁ <+: l₂ → l₁ <+ l₂

source

theorem list.sublist_of_suffix {α : Type u} {l₁ l₂ : list α} :

l₁ <:+ l₂ → l₁ <+ l₂

source

theorem list.reverse_suffix {α : Type u} {l₁ l₂ : list α} :

l₁.reverse <:+ l₂.reverse ↔ l₁ <+: l₂

source

theorem list.reverse_prefix {α : Type u} {l₁ l₂ : list α} :

l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂

source

theorem list.length_le_of_infix {α : Type u} {l₁ l₂ : list α} :

l₁ <:+: l₂ → l₁.length ≤ l₂.length

source

theorem list.eq_nil_of_infix_nil {α : Type u} {l : list α} :

l <:+: list.nil → l = list.nil

source

theorem list.eq_nil_of_prefix_nil {α : Type u} {l : list α} :

l <+: list.nil → l = list.nil

source

theorem list.eq_nil_of_suffix_nil {α : Type u} {l : list α} :

l <:+ list.nil → l = list.nil

source

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

l₁ <:+: l₂ ↔ ∃ (t : list α), l₁ <+: t ∧ t <:+ l₂

source

theorem list.eq_of_infix_of_length_eq {α : Type u} {l₁ l₂ : list α} :

l₁ <:+: l₂ → l₁.length = l₂.length → l₁ = l₂

source

theorem list.eq_of_prefix_of_length_eq {α : Type u} {l₁ l₂ : list α} :

l₁ <+: l₂ → l₁.length = l₂.length → l₁ = l₂

source

theorem list.eq_of_suffix_of_length_eq {α : Type u} {l₁ l₂ : list α} :

l₁ <:+ l₂ → l₁.length = l₂.length → l₁ = l₂

source

theorem list.prefix_of_prefix_length_le {α : Type u} {l₁ l₂ l₃ : list α} :

l₁ <+: l₃ → l₂ <+: l₃ → l₁.length ≤ l₂.length → l₁ <+: l₂

source

theorem list.prefix_or_prefix_of_prefix {α : Type u} {l₁ l₂ l₃ : list α} :

l₁ <+: l₃ → l₂ <+: l₃ → l₁ <+: l₂ ∨ l₂ <+: l₁

source

theorem list.suffix_of_suffix_length_le {α : Type u} {l₁ l₂ l₃ : list α} :

l₁ <:+ l₃ → l₂ <:+ l₃ → l₁.length ≤ l₂.length → l₁ <:+ l₂

source

theorem list.suffix_or_suffix_of_suffix {α : Type u} {l₁ l₂ l₃ : list α} :

l₁ <:+ l₃ → l₂ <:+ l₃ → l₁ <:+ l₂ ∨ l₂ <:+ l₁

source

theorem list.infix_of_mem_join {α : Type u} {L : list (list α)} {l : list α} :

l ∈ L → l <:+: L.join

source

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

l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂

source

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

a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂

source

theorem list.take_prefix {α : Type u} (n : ℕ) (l : list α) :

list.take n l <+: l

source

theorem list.drop_suffix {α : Type u} (n : ℕ) (l : list α) :

list.drop n l <:+ l

source

theorem list.tail_suffix {α : Type u} (l : list α) :

l.tail <:+ l

source

theorem list.tail_subset {α : Type u} (l : list α) :

l.tail ⊆ l

source

theorem list.prefix_iff_eq_append {α : Type u} {l₁ l₂ : list α} :

l₁ <+: l₂ ↔ l₁ ++ list.drop l₁.length l₂ = l₂

source

theorem list.suffix_iff_eq_append {α : Type u} {l₁ l₂ : list α} :

l₁ <:+ l₂ ↔ list.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂

source

theorem list.prefix_iff_eq_take {α : Type u} {l₁ l₂ : list α} :

l₁ <+: l₂ ↔ l₁ = list.take l₁.length l₂

source

theorem list.suffix_iff_eq_drop {α : Type u} {l₁ l₂ : list α} :

l₁ <:+ l₂ ↔ l₁ = list.drop (l₂.length - l₁.length) l₂

source

@[instance]

def list.decidable_prefix {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

decidable (l₁ <+: l₂)

Equations

(a :: l₁).decidable_prefix (b :: l₂) = dite (a = b) (λ (h : a = b), decidable_of_iff (l₁ <+: l₂) _) (λ (h : ¬a = b), decidable.is_false _)
(a :: l₁).decidable_prefix list.nil = decidable.is_false _
list.nil.decidable_prefix l₂ = decidable.is_true _

source

@[instance]

def list.decidable_suffix {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

decidable (l₁ <:+ l₂)

Equations

(hd :: tl).decidable_suffix (hd_1 :: tl_1) = let len1 : ℕ := (hd :: tl).length, len2 : ℕ := (hd_1 :: tl_1).length in dite (len1 ≤ len2) (λ (hl : len1 ≤ len2), decidable_of_iff' (hd :: tl = list.drop (len2 - len1) (hd_1 :: tl_1)) _) (λ (hl : ¬len1 ≤ len2), decidable.is_false _)
(a :: l₁).decidable_suffix list.nil = decidable.is_false _
list.nil.decidable_suffix l₂ = decidable.is_true _

source

@[simp]

theorem list.mem_inits {α : Type u} (s t : list α) :

s ∈ t.inits ↔ s <+: t

source

@[simp]

theorem list.mem_tails {α : Type u} (s t : list α) :

s ∈ t.tails ↔ s <:+ t

source

@[instance]

def list.decidable_infix {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

decidable (l₁ <:+: l₂)

Equations

(hd :: tl).decidable_infix (hd_1 :: tl_1) = decidable_of_decidable_of_iff (list.decidable_bex (λ (t : list α), hd :: tl <+: t) (hd_1 :: tl_1).tails) _
(a :: l₁).decidable_infix list.nil = decidable.is_false _
list.nil.decidable_infix l₂ = decidable.is_true _

source

@[simp]

theorem list.sublists'_nil {α : Type u} :

list.nil.sublists' = [list.nil]

source

@[simp]

theorem list.sublists'_singleton {α : Type u} (a : α) :

[a].sublists' = [list.nil, [a]]

source

theorem list.map_sublists'_aux {α : Type u} {β : Type v} {γ : Type w} (g : list β → list γ) (l : list α) (f : list α → list β) (r : list (list β)) :

list.map g (l.sublists'_aux f r) = l.sublists'_aux (g ∘ f) (list.map g r)

source

theorem list.sublists'_aux_append {α : Type u} {β : Type v} (r' : list (list β)) (l : list α) (f : list α → list β) (r : list (list β)) :

l.sublists'_aux f (r ++ r') = l.sublists'_aux f r ++ r'

source

theorem list.sublists'_aux_eq_sublists' {α : Type u} {β : Type v} (l : list α) (f : list α → list β) (r : list (list β)) :

l.sublists'_aux f r = list.map f l.sublists' ++ r

source

@[simp]

theorem list.sublists'_cons {α : Type u} (a : α) (l : list α) :

(a :: l).sublists' = l.sublists' ++ list.map (list.cons a) l.sublists'

source

@[simp]

theorem list.mem_sublists' {α : Type u} {s t : list α} :

s ∈ t.sublists' ↔ s <+ t

source

@[simp]

theorem list.length_sublists' {α : Type u} (l : list α) :

l.sublists'.length = 2 ^ l.length

source

@[simp]

theorem list.sublists_nil {α : Type u} :

list.nil.sublists = [list.nil]

source

@[simp]

theorem list.sublists_singleton {α : Type u} (a : α) :

[a].sublists = [list.nil, [a]]

source

theorem list.sublists_aux₁_eq_sublists_aux {α : Type u} {β : Type v} (l : list α) (f : list α → list β) :

l.sublists_aux₁ f = l.sublists_aux (λ (ys : list α) (r : list β), f ys ++ r)

source

theorem list.sublists_aux_cons_eq_sublists_aux₁ {α : Type u} (l : list α) :

l.sublists_aux list.cons = l.sublists_aux₁ (λ (x : list α), [x])

source

theorem list.sublists_aux_eq_foldr.aux {α : Type u} {β : Type v} {a : α} {l : list α} (IH₁ : ∀ (f : list α → list β → list β), l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons)) (IH₂ : ∀ (f : list α → list (list α) → list (list α)), l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons)) (f : list α → list β → list β) :

(a :: l).sublists_aux f = list.foldr f list.nil ((a :: l).sublists_aux list.cons)

source

theorem list.sublists_aux_eq_foldr {α : Type u} {β : Type v} (l : list α) (f : list α → list β → list β) :

l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons)

source

theorem list.sublists_aux_cons_cons {α : Type u} (l : list α) (a : α) :

(a :: l).sublists_aux list.cons = [a] :: list.foldr (λ (ys : list α) (r : list (list α)), ys :: (a :: ys) :: r) list.nil (l.sublists_aux list.cons)

source

theorem list.sublists_aux₁_append {α : Type u} {β : Type v} (l₁ l₂ : list α) (f : list α → list β) :

(l₁ ++ l₂).sublists_aux₁ f = l₁.sublists_aux₁ f ++ l₂.sublists_aux₁ (λ (x : list α), f x ++ l₁.sublists_aux₁ (f ∘ λ (_x : list α), _x ++ x))

source

theorem list.sublists_aux₁_concat {α : Type u} {β : Type v} (l : list α) (a : α) (f : list α → list β) :

(l ++ [a]).sublists_aux₁ f = l.sublists_aux₁ f ++ f [a] ++ l.sublists_aux₁ (λ (x : list α), f (x ++ [a]))

source

theorem list.sublists_aux₁_bind {α : Type u} {β : Type v} {γ : Type w} (l : list α) (f : list α → list β) (g : β → list γ) :

(l.sublists_aux₁ f).bind g = l.sublists_aux₁ (λ (x : list α), (f x).bind g)

source

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

(l₁ ++ l₂).sublists_aux list.cons = l₁.sublists_aux list.cons ++ (l₂.sublists_aux list.cons >>= λ (x : list α), (λ (_x : list α), _x ++ x) <$> l₁.sublists)

source

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

(l₁ ++ l₂).sublists = l₂.sublists >>= λ (x : list α), (λ (_x : list α), _x ++ x) <$> l₁.sublists

source

@[simp]

theorem list.sublists_concat {α : Type u} (l : list α) (a : α) :

(l ++ [a]).sublists = l.sublists ++ list.map (λ (x : list α), x ++ [a]) l.sublists

source

theorem list.sublists_reverse {α : Type u} (l : list α) :

l.reverse.sublists = list.map list.reverse l.sublists'

source

theorem list.sublists_eq_sublists' {α : Type u} (l : list α) :

l.sublists = list.map list.reverse l.reverse.sublists'

source

theorem list.sublists'_reverse {α : Type u} (l : list α) :

l.reverse.sublists' = list.map list.reverse l.sublists

source

theorem list.sublists'_eq_sublists {α : Type u} (l : list α) :

l.sublists' = list.map list.reverse l.reverse.sublists

source

theorem list.sublists_aux_ne_nil {α : Type u} (l : list α) :

list.nil ∉ l.sublists_aux list.cons

source

@[simp]

theorem list.mem_sublists {α : Type u} {s t : list α} :

s ∈ t.sublists ↔ s <+ t

source

@[simp]

theorem list.length_sublists {α : Type u} (l : list α) :

l.sublists.length = 2 ^ l.length

source

theorem list.map_ret_sublist_sublists {α : Type u} (l : list α) :

list.map list.ret l <+ l.sublists

source

def list.sublists_len_aux {α : Type u_1} {β : Type u_2} :

ℕ → list α → (list α → β) → list β → list β

Auxiliary function to construct the list of all sublists of a given length. Given an integer n, a list l, a function f and an auxiliary list L, it returns the list made of of f applied to all sublists of l of length n, concatenated with L.

Equations

list.sublists_len_aux (n + 1) (a :: l) f r = list.sublists_len_aux (n + 1) l f (list.sublists_len_aux n l (f ∘ list.cons a) r)
list.sublists_len_aux (n + 1) list.nil f r = r
list.sublists_len_aux 0 (hd :: tl) f r = f list.nil :: r
list.sublists_len_aux 0 list.nil f r = f list.nil :: r

source

def list.sublists_len {α : Type u_1} :

ℕ → list α → list (list α)

The list of all sublists of a list l that are of length n. For instance, for l = [0, 1, 2, 3] and n = 2, one gets [[2, 3], [1, 3], [1, 2], [0, 3], [0, 2], [0, 1]].

Equations

list.sublists_len n l = list.sublists_len_aux n l id list.nil

source

theorem list.sublists_len_aux_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} (n : ℕ) (l : list α) (f : list α → β) (g : β → γ) (r : list β) (s : list γ) :

list.sublists_len_aux n l (g ∘ f) (list.map g r ++ s) = list.map g (list.sublists_len_aux n l f r) ++ s

source

theorem list.sublists_len_aux_eq {α : Type u_1} {β : Type u_2} (l : list α) (n : ℕ) (f : list α → β) (r : list β) :

list.sublists_len_aux n l f r = list.map f (list.sublists_len n l) ++ r

source

theorem list.sublists_len_aux_zero {β : Type v} {α : Type u_1} (l : list α) (f : list α → β) (r : list β) :

list.sublists_len_aux 0 l f r = f list.nil :: r

source

@[simp]

theorem list.sublists_len_zero {α : Type u_1} (l : list α) :

list.sublists_len 0 l = [list.nil]

source

@[simp]

theorem list.sublists_len_succ_nil {α : Type u_1} (n : ℕ) :

list.sublists_len (n + 1) list.nil = list.nil

source

@[simp]

theorem list.sublists_len_succ_cons {α : Type u_1} (n : ℕ) (a : α) (l : list α) :

list.sublists_len (n + 1) (a :: l) = list.sublists_len (n + 1) l ++ list.map (list.cons a) (list.sublists_len n l)

source

@[simp]

theorem list.length_sublists_len {α : Type u_1} (n : ℕ) (l : list α) :

(list.sublists_len n l).length = l.length.choose n

source

theorem list.sublists_len_sublist_sublists' {α : Type u_1} (n : ℕ) (l : list α) :

list.sublists_len n l <+ l.sublists'

source

theorem list.sublists_len_sublist_of_sublist {α : Type u_1} (n : ℕ) {l₁ l₂ : list α} :

l₁ <+ l₂ → list.sublists_len n l₁ <+ list.sublists_len n l₂

source

theorem list.length_of_sublists_len {α : Type u_1} {n : ℕ} {l l' : list α} :

l' ∈ list.sublists_len n l → l'.length = n

source

theorem list.mem_sublists_len_self {α : Type u_1} {l l' : list α} :

l' <+ l → l' ∈ list.sublists_len l'.length l

source

@[simp]

theorem list.mem_sublists_len {α : Type u_1} {n : ℕ} {l l' : list α} :

l' ∈ list.sublists_len n l ↔ l' <+ l ∧ l'.length = n

source

@[simp]

theorem list.permutations_aux_nil {α : Type u} (is : list α) :

list.nil.permutations_aux is = list.nil

source

@[simp]

theorem list.permutations_aux_cons {α : Type u} (t : α) (ts is : list α) :

(t :: ts).permutations_aux is = list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) (ts.permutations_aux (t :: is)) is.permutations

source

@[simp]

theorem list.insert_nil {α : Type u} [decidable_eq α] (a : α) :

has_insert.insert a list.nil = [a]

source

theorem list.insert.def {α : Type u} [decidable_eq α] (a : α) (l : list α) :

has_insert.insert a l = ite (a ∈ l) l (a :: l)

source

@[simp]

theorem list.insert_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∈ l → has_insert.insert a l = l

source

@[simp]

theorem list.insert_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∉ l → has_insert.insert a l = a :: l

source

@[simp]

theorem list.mem_insert_iff {α : Type u} [decidable_eq α] {a b : α} {l : list α} :

a ∈ has_insert.insert b l ↔ a = b ∨ a ∈ l

source

@[simp]

theorem list.suffix_insert {α : Type u} [decidable_eq α] (a : α) (l : list α) :

l <:+ has_insert.insert a l

source

@[simp]

theorem list.mem_insert_self {α : Type u} [decidable_eq α] (a : α) (l : list α) :

a ∈ has_insert.insert a l

source

theorem list.mem_insert_of_mem {α : Type u} [decidable_eq α] {a b : α} {l : list α} :

a ∈ l → a ∈ has_insert.insert b l

source

theorem list.eq_or_mem_of_mem_insert {α : Type u} [decidable_eq α] {a b : α} {l : list α} :

a ∈ has_insert.insert b l → a = b ∨ a ∈ l

source

@[simp]

theorem list.length_insert_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∈ l → (has_insert.insert a l).length = l.length

source

@[simp]

theorem list.length_insert_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∉ l → (has_insert.insert a l).length = l.length + 1

source

@[simp]

theorem list.erasep_nil {α : Type u} {p : α → Prop} [decidable_pred p] :

list.erasep p list.nil = list.nil

source

theorem list.erasep_cons {α : Type u} {p : α → Prop} [decidable_pred p] (a : α) (l : list α) :

list.erasep p (a :: l) = ite (p a) l (a :: list.erasep p l)

source

@[simp]

theorem list.erasep_cons_of_pos {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

p a → list.erasep p (a :: l) = l

source

@[simp]

theorem list.erasep_cons_of_neg {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

¬p a → list.erasep p (a :: l) = a :: list.erasep p l

source

theorem list.erasep_of_forall_not {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :

(∀ (a : α), a ∈ l → ¬p a) → list.erasep p l = l

source

theorem list.exists_of_erasep {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} :

a ∈ l → p a → (∃ (a : α) (l₁ l₂ : list α), (∀ (b : α), b ∈ l₁ → ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ list.erasep p l = l₁ ++ l₂)

source

theorem list.exists_or_eq_self_of_erasep {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :

list.erasep p l = l ∨ ∃ (a : α) (l₁ l₂ : list α), (∀ (b : α), b ∈ l₁ → ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ list.erasep p l = l₁ ++ l₂

source

@[simp]

theorem list.length_erasep_of_mem {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} :

a ∈ l → p a → (list.erasep p l).length = l.length.pred

source

theorem list.erasep_append_left {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (pa : p a) {l₁ : list α} (l₂ : list α) :

a ∈ l₁ → list.erasep p (l₁ ++ l₂) = list.erasep p l₁ ++ l₂

source

theorem list.erasep_append_right {α : Type u} {p : α → Prop} [decidable_pred p] {l₁ : list α} (l₂ : list α) :

(∀ (b : α), b ∈ l₁ → ¬p b) → list.erasep p (l₁ ++ l₂) = l₁ ++ list.erasep p l₂

source

theorem list.erasep_sublist {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :

list.erasep p l <+ l

source

theorem list.erasep_subset {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :

list.erasep p l ⊆ l

source

theorem list.sublist.erasep {α : Type u} {p : α → Prop} [decidable_pred p] {l₁ l₂ : list α} :

l₁ <+ l₂ → list.erasep p l₁ <+ list.erasep p l₂

source

theorem list.mem_of_mem_erasep {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

a ∈ list.erasep p l → a ∈ l

source

@[simp]

theorem list.mem_erasep_of_neg {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :

¬p a → (a ∈ list.erasep p l ↔ a ∈ l)

source

theorem list.erasep_map {α : Type u} {β : Type v} {p : α → Prop} [decidable_pred p] (f : β → α) (l : list β) :

list.erasep p (list.map f l) = list.map f (list.erasep (p ∘ f) l)

source

@[simp]

theorem list.extractp_eq_find_erasep {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :

list.extractp p l = (list.find p l, list.erasep p l)

source

@[simp]

theorem list.erase_nil {α : Type u} [decidable_eq α] (a : α) :

list.nil.erase a = list.nil

source

theorem list.erase_cons {α : Type u} [decidable_eq α] (a b : α) (l : list α) :

(b :: l).erase a = ite (b = a) l (b :: l.erase a)

source

@[simp]

theorem list.erase_cons_head {α : Type u} [decidable_eq α] (a : α) (l : list α) :

(a :: l).erase a = l

source

@[simp]

theorem list.erase_cons_tail {α : Type u} [decidable_eq α] {a b : α} (l : list α) :

b ≠ a → (b :: l).erase a = b :: l.erase a

source

theorem list.erase_eq_erasep {α : Type u} [decidable_eq α] (a : α) (l : list α) :

l.erase a = list.erasep (eq a) l

source

@[simp]

theorem list.erase_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∉ l → l.erase a = l

source

theorem list.exists_erase_eq {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∈ l → (∃ (l₁ l₂ : list α), a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂)

source

@[simp]

theorem list.length_erase_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :

a ∈ l → (l.erase a).length = l.length.pred

source

theorem list.erase_append_left {α : Type u} [decidable_eq α] {a : α} {l₁ : list α} (l₂ : list α) :

a ∈ l₁ → (l₁ ++ l₂).erase a = l₁.erase a ++ l₂

source

theorem list.erase_append_right {α : Type u} [decidable_eq α] {a : α} {l₁ : list α} (l₂ : list α) :

a ∉ l₁ → (l₁ ++ l₂).erase a = l₁ ++ l₂.erase a

source

theorem list.erase_sublist {α : Type u} [decidable_eq α] (a : α) (l : list α) :

l.erase a <+ l

source

theorem list.erase_subset {α : Type u} [decidable_eq α] (a : α) (l : list α) :

l.erase a ⊆ l

source

theorem list.sublist.erase {α : Type u} [decidable_eq α] (a : α) {l₁ l₂ : list α} :

l₁ <+ l₂ → l₁.erase a <+ l₂.erase a

source

theorem list.mem_of_mem_erase {α : Type u} [decidable_eq α] {a b : α} {l : list α} :

a ∈ l.erase b → a ∈ l

source

@[simp]

theorem list.mem_erase_of_ne {α : Type u} [decidable_eq α] {a b : α} {l : list α} :

a ≠ b → (a ∈ l.erase b ↔ a ∈ l)

source

theorem list.erase_comm {α : Type u} [decidable_eq α] (a b : α) (l : list α) :

(l.erase a).erase b = (l.erase b).erase a

source

theorem list.map_erase {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {f : α → β} (finj : function.injective f) {a : α} (l : list α) :

list.map f (l.erase a) = (list.map f l).erase (f a)

source

theorem list.map_foldl_erase {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {f : α → β} (finj : function.injective f) {l₁ l₂ : list α} :

list.map f (list.foldl list.erase l₁ l₂) = list.foldl (λ (l : list β) (a : α), l.erase (f a)) (list.map f l₁) l₂

source

@[simp]

theorem list.count_erase_self {α : Type u} [decidable_eq α] (a : α) (s : list α) :

list.count a (s.erase a) = (list.count a s).pred

source

@[simp]

theorem list.count_erase_of_ne {α : Type u} [decidable_eq α] {a b : α} (ab : a ≠ b) (s : list α) :

list.count a (s.erase b) = list.count a s

source

@[simp]

theorem list.diff_nil {α : Type u} [decidable_eq α] (l : list α) :

l.diff list.nil = l

source

@[simp]

theorem list.diff_cons {α : Type u} [decidable_eq α] (l₁ l₂ : list α) (a : α) :

l₁.diff (a :: l₂) = (l₁.erase a).diff l₂

source

@[simp]

theorem list.nil_diff {α : Type u} [decidable_eq α] (l : list α) :

list.nil.diff l = list.nil

source

theorem list.diff_eq_foldl {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

l₁.diff l₂ = list.foldl list.erase l₁ l₂

source

@[simp]

theorem list.diff_append {α : Type u} [decidable_eq α] (l₁ l₂ l₃ : list α) :

l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃

source

@[simp]

theorem list.map_diff {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {f : α → β} (finj : function.injective f) {l₁ l₂ : list α} :

list.map f (l₁.diff l₂) = (list.map f l₁).diff (list.map f l₂)

source

theorem list.diff_sublist {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

l₁.diff l₂ <+ l₁

source

theorem list.diff_subset {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

l₁.diff l₂ ⊆ l₁

source

theorem list.mem_diff_of_mem {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :

a ∈ l₁ → a ∉ l₂ → a ∈ l₁.diff l₂

source

theorem list.sublist.diff_right {α : Type u} [decidable_eq α] {l₁ l₂ l₃ : list α} :

l₁ <+ l₂ → l₁.diff l₃ <+ l₂.diff l₃

source

theorem list.erase_diff_erase_sublist_of_sublist {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :

l₁ <+ l₂ → (l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁

source

theorem list.length_enum_from {α : Type u} (n : ℕ) (l : list α) :

(list.enum_from n l).length = l.length

source

theorem list.length_enum {α : Type u} (l : list α) :

l.enum.length = l.length

source

@[simp]

theorem list.enum_from_nth {α : Type u} (n : ℕ) (l : list α) (m : ℕ) :

(list.enum_from n l).nth m = (λ (a : α), (n + m, a)) <$> l.nth m

source

@[simp]

theorem list.enum_nth {α : Type u} (l : list α) (n : ℕ) :

l.enum.nth n = (λ (a : α), (n, a)) <$> l.nth n

source

@[simp]

theorem list.enum_from_map_snd {α : Type u} (n : ℕ) (l : list α) :

list.map prod.snd (list.enum_from n l) = l

source

@[simp]

theorem list.enum_map_snd {α : Type u} (l : list α) :

list.map prod.snd l.enum = l

source

theorem list.mem_enum_from {α : Type u} {x : α} {i j : ℕ} (xs : list α) :

(i, x) ∈ list.enum_from j xs → j ≤ i ∧ i < j + xs.length ∧ x ∈ xs

source

@[simp]

theorem list.nil_product {α : Type u} {β : Type v} (l : list β) :

list.nil.product l = list.nil

source

@[simp]

theorem list.product_cons {α : Type u} {β : Type v} (a : α) (l₁ : list α) (l₂ : list β) :

(a :: l₁).product l₂ = list.map (λ (b : β), (a, b)) l₂ ++ l₁.product l₂

source

@[simp]

theorem list.product_nil {α : Type u} {β : Type v} (l : list α) :

l.product list.nil = list.nil

source

@[simp]

theorem list.mem_product {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} {a : α} {b : β} :

(a, b) ∈ l₁.product l₂ ↔ a ∈ l₁ ∧ b ∈ l₂

source

theorem list.length_product {α : Type u} {β : Type v} (l₁ : list α) (l₂ : list β) :

(l₁.product l₂).length = l₁.length * l₂.length

source

@[simp]

theorem list.nil_sigma {α : Type u} {σ : α → Type u_1} (l : Π (a : α), list (σ a)) :

list.nil.sigma l = list.nil

source

@[simp]

theorem list.sigma_cons {α : Type u} {σ : α → Type u_1} (a : α) (l₁ : list α) (l₂ : Π (a : α), list (σ a)) :

(a :: l₁).sigma l₂ = list.map (sigma.mk a) (l₂ a) ++ l₁.sigma l₂

source

@[simp]

theorem list.sigma_nil {α : Type u} {σ : α → Type u_1} (l : list α) :

l.sigma (λ (a : α), list.nil) = list.nil

source

@[simp]

theorem list.mem_sigma {α : Type u} {σ : α → Type u_1} {l₁ : list α} {l₂ : Π (a : α), list (σ a)} {a : α} {b : σ a} :

⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

source

theorem list.length_sigma {α : Type u} {σ : α → Type u_1} (l₁ : list α) (l₂ : Π (a : α), list (σ a)) :

(l₁.sigma l₂).length = (list.map (λ (a : α), (l₂ a).length) l₁).sum

source

theorem list.disjoint.symm {α : Type u} {l₁ l₂ : list α} :

l₁.disjoint l₂ → l₂.disjoint l₁

source

theorem list.disjoint_comm {α : Type u} {l₁ l₂ : list α} :

l₁.disjoint l₂ ↔ l₂.disjoint l₁

source

theorem list.disjoint_left {α : Type u} {l₁ l₂ : list α} :

l₁.disjoint l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∉ l₂

source

theorem list.disjoint_right {α : Type u} {l₁ l₂ : list α} :

l₁.disjoint l₂ ↔ ∀ {a : α}, a ∈ l₂ → a ∉ l₁

source

theorem list.disjoint_iff_ne {α : Type u} {l₁ l₂ : list α} :

l₁.disjoint l₂ ↔ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → a ≠ b

source

theorem list.disjoint_of_subset_left {α : Type u} {l₁ l₂ l : list α} :

l₁ ⊆ l → l.disjoint l₂ → l₁.disjoint l₂

source

theorem list.disjoint_of_subset_right {α : Type u} {l₁ l₂ l : list α} :

l₂ ⊆ l → l₁.disjoint l → l₁.disjoint l₂

source

theorem list.disjoint_of_disjoint_cons_left {α : Type u} {a : α} {l₁ l₂ : list α} :

(a :: l₁).disjoint l₂ → l₁.disjoint l₂

source

theorem list.disjoint_of_disjoint_cons_right {α : Type u} {a : α} {l₁ l₂ : list α} :

l₁.disjoint (a :: l₂) → l₁.disjoint l₂

source

@[simp]

theorem list.disjoint_nil_left {α : Type u} (l : list α) :

list.nil.disjoint l

source

@[simp]

theorem list.disjoint_nil_right {α : Type u} (l : list α) :

l.disjoint list.nil

source

@[simp]

theorem list.singleton_disjoint {α : Type u} {l : list α} {a : α} :

[a].disjoint l ↔ a ∉ l

source

@[simp]

theorem list.disjoint_singleton {α : Type u} {l : list α} {a : α} :

l.disjoint [a] ↔ a ∉ l

source

@[simp]

theorem list.disjoint_append_left {α : Type u} {l₁ l₂ l : list α} :

(l₁ ++ l₂).disjoint l ↔ l₁.disjoint l ∧ l₂.disjoint l

source

@[simp]

theorem list.disjoint_append_right {α : Type u} {l₁ l₂ l : list α} :

l.disjoint (l₁ ++ l₂) ↔ l.disjoint l₁ ∧ l.disjoint l₂

source

@[simp]

theorem list.disjoint_cons_left {α : Type u} {a : α} {l₁ l₂ : list α} :

(a :: l₁).disjoint l₂ ↔ a ∉ l₂ ∧ l₁.disjoint l₂

source

@[simp]

theorem list.disjoint_cons_right {α : Type u} {a : α} {l₁ l₂ : list α} :

l₁.disjoint (a :: l₂) ↔ a ∉ l₁ ∧ l₁.disjoint l₂

source

theorem list.disjoint_of_disjoint_append_left_left {α : Type u} {l₁ l₂ l : list α} :

(l₁ ++ l₂).disjoint l → l₁.disjoint l

source

theorem list.disjoint_of_disjoint_append_left_right {α : Type u} {l₁ l₂ l : list α} :

(l₁ ++ l₂).disjoint l → l₂.disjoint l

source

theorem list.disjoint_of_disjoint_append_right_left {α : Type u} {l₁ l₂ l : list α} :

l.disjoint (l₁ ++ l₂) → l.disjoint l₁

source

theorem list.disjoint_of_disjoint_append_right_right {α : Type u} {l₁ l₂ l : list α} :

l.disjoint (l₁ ++ l₂) → l.disjoint l₂

source

@[simp]

theorem list.nil_union {α : Type u} [decidable_eq α] (l : list α) :

list.nil ∪ l = l

source

@[simp]

theorem list.cons_union {α : Type u} [decidable_eq α] (l₁ l₂ : list α) (a : α) :

a :: l₁ ∪ l₂ = has_insert.insert a (l₁ ∪ l₂)

source

@[simp]

theorem list.mem_union {α : Type u} [decidable_eq α] {l₁ l₂ : list α} {a : α} :

a ∈ l₁ ∪ l₂ ↔ a ∈ l₁ ∨ a ∈ l₂

source

theorem list.mem_union_left {α : Type u} [decidable_eq α] {a : α} {l₁ : list α} (h : a ∈ l₁) (l₂ : list α) :

a ∈ l₁ ∪ l₂

source

theorem list.mem_union_right {α : Type u} [decidable_eq α] {a : α} (l₁ : list α) {l₂ : list α} :

a ∈ l₂ → a ∈ l₁ ∪ l₂

source

theorem list.sublist_suffix_of_union {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

∃ (t : list α), t <+ l₁ ∧ t ++ l₂ = l₁ ∪ l₂

source

theorem list.suffix_union_right {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

l₂ <:+ l₁ ∪ l₂

source

theorem list.union_sublist_append {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

l₁ ∪ l₂ <+ l₁ ++ l₂

source

theorem list.forall_mem_union {α : Type u} [decidable_eq α] {p : α → Prop} {l₁ l₂ : list α} :

(∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

source

theorem list.forall_mem_of_forall_mem_union_left {α : Type u} [decidable_eq α] {p : α → Prop} {l₁ l₂ : list α} (h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x) (x : α) :

x ∈ l₁ → p x

source

theorem list.forall_mem_of_forall_mem_union_right {α : Type u} [decidable_eq α] {p : α → Prop} {l₁ l₂ : list α} (h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x) (x : α) :

x ∈ l₂ → p x

source

@[simp]

theorem list.inter_nil {α : Type u} [decidable_eq α] (l : list α) :

list.nil ∩ l = list.nil

source

@[simp]

theorem list.inter_cons_of_mem {α : Type u} [decidable_eq α] {a : α} (l₁ : list α) {l₂ : list α} :

a ∈ l₂ → (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

source

@[simp]

theorem list.inter_cons_of_not_mem {α : Type u} [decidable_eq α] {a : α} (l₁ : list α) {l₂ : list α} :

a ∉ l₂ → (a :: l₁) ∩ l₂ = l₁ ∩ l₂

source

theorem list.mem_of_mem_inter_left {α : Type u} [decidable_eq α] {l₁ l₂ : list α} {a : α} :

a ∈ l₁ ∩ l₂ → a ∈ l₁

source

theorem list.mem_of_mem_inter_right {α : Type u} [decidable_eq α] {l₁ l₂ : list α} {a : α} :

a ∈ l₁ ∩ l₂ → a ∈ l₂

source

theorem list.mem_inter_of_mem_of_mem {α : Type u} [decidable_eq α] {l₁ l₂ : list α} {a : α} :

a ∈ l₁ → a ∈ l₂ → a ∈ l₁ ∩ l₂

source

@[simp]

theorem list.mem_inter {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :

a ∈ l₁ ∩ l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

source

theorem list.inter_subset_left {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

l₁ ∩ l₂ ⊆ l₁

source

theorem list.inter_subset_right {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

l₁ ∩ l₂ ⊆ l₂

source

theorem list.subset_inter {α : Type u} [decidable_eq α] {l l₁ l₂ : list α} :

l ⊆ l₁ → l ⊆ l₂ → l ⊆ l₁ ∩ l₂

source

theorem list.inter_eq_nil_iff_disjoint {α : Type u} [decidable_eq α] {l₁ l₂ : list α} :

l₁ ∩ l₂ = list.nil ↔ l₁.disjoint l₂

source

theorem list.forall_mem_inter_of_forall_left {α : Type u} [decidable_eq α] {p : α → Prop} {l₁ : list α} (h : ∀ (x : α), x ∈ l₁ → p x) (l₂ : list α) (x : α) :

x ∈ l₁ ∩ l₂ → p x

source

theorem list.forall_mem_inter_of_forall_right {α : Type u} [decidable_eq α] {p : α → Prop} (l₁ : list α) {l₂ : list α} (h : ∀ (x : α), x ∈ l₂ → p x) (x : α) :

x ∈ l₁ ∩ l₂ → p x

source