mathlib documentation

data.list.count

Counting in lists #

This file proves basic properties of list.countp and list.count, which count the number of elements of a list satisfying a predicate and equal to a given element respectively. Their definitions can be found in data.list.defs.

@[simp]
theorem list.countp_nil {α : Type u_1} (p : α → Prop) [decidable_pred p] :
@[simp]
theorem list.countp_cons_of_pos {α : Type u_1} (p : α → Prop) [decidable_pred p] {a : α} (l : list α) (pa : p a) :
list.countp p (a :: l) = list.countp p l + 1
@[simp]
theorem list.countp_cons_of_neg {α : Type u_1} (p : α → Prop) [decidable_pred p] {a : α} (l : list α) (pa : ¬p a) :
theorem list.countp_cons {α : Type u_1} (p : α → Prop) [decidable_pred p] (a : α) (l : list α) :
list.countp p (a :: l) = list.countp p l + ite (p a) 1 0
theorem list.length_eq_countp_add_countp {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :
l.length = list.countp p l + list.countp (λ (a : α), ¬p a) l
theorem list.countp_eq_length_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :
theorem list.countp_le_length {α : Type u_1} {l : list α} (p : α → Prop) [decidable_pred p] :
@[simp]
theorem list.countp_append {α : Type u_1} (p : α → Prop) [decidable_pred p] (l₁ l₂ : list α) :
list.countp p (l₁ ++ l₂) = list.countp p l₁ + list.countp p l₂
theorem list.countp_pos {α : Type u_1} (p : α → Prop) [decidable_pred p] {l : list α} :
0 < list.countp p l ∃ (a : α) (H : a l), p a
theorem list.countp_eq_zero {α : Type u_1} (p : α → Prop) [decidable_pred p] {l : list α} :
list.countp p l = 0 ∀ (a : α), a l¬p a
theorem list.countp_eq_length {α : Type u_1} (p : α → Prop) [decidable_pred p] {l : list α} :
list.countp p l = l.length ∀ (a : α), a lp a
theorem list.length_filter_lt_length_iff_exists {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :
(list.filter p l).length < l.length ∃ (x : α) (H : x l), ¬p x
theorem list.sublist.countp_le {α : Type u_1} {l₁ l₂ : list α} (p : α → Prop) [decidable_pred p] (s : l₁ <+ l₂) :
@[simp]
theorem list.countp_filter {α : Type u_1} (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
@[simp]
theorem list.countp_true {α : Type u_1} {l : list α} :
list.countp (λ (_x : α), true) l = l.length
@[simp]
theorem list.countp_false {α : Type u_1} {l : list α} :
list.countp (λ (_x : α), false) l = 0

count #

@[simp]
theorem list.count_nil {α : Type u_1} [decidable_eq α] (a : α) :
theorem list.count_cons {α : Type u_1} [decidable_eq α] (a b : α) (l : list α) :
list.count a (b :: l) = ite (a = b) (list.count a l).succ (list.count a l)
theorem list.count_cons' {α : Type u_1} [decidable_eq α] (a b : α) (l : list α) :
list.count a (b :: l) = list.count a l + ite (a = b) 1 0
@[simp]
theorem list.count_cons_self {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
list.count a (a :: l) = (list.count a l).succ
@[simp]
theorem list.count_cons_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (h : a b) (l : list α) :
theorem list.count_tail {α : Type u_1} [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
theorem list.count_le_length {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
theorem list.sublist.count_le {α : Type u_1} {l₁ l₂ : list α} [decidable_eq α] (h : l₁ <+ l₂) (a : α) :
list.count a l₁ list.count a l₂
theorem list.count_le_count_cons {α : Type u_1} [decidable_eq α] (a b : α) (l : list α) :
theorem list.count_singleton {α : Type u_1} [decidable_eq α] (a : α) :
list.count a [a] = 1
theorem list.count_singleton' {α : Type u_1} [decidable_eq α] (a b : α) :
list.count a [b] = ite (a = b) 1 0
@[simp]
theorem list.count_append {α : Type u_1} [decidable_eq α] (a : α) (l₁ l₂ : list α) :
list.count a (l₁ ++ l₂) = list.count a l₁ + list.count a l₂
theorem list.count_concat {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
@[simp]
theorem list.count_pos {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
0 < list.count a l a l
@[simp]
theorem list.one_le_count_iff_mem {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
1 list.count a l a l
@[simp]
theorem list.count_eq_zero_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {l : list α} (h : a l) :
theorem list.not_mem_of_count_eq_zero {α : Type u_1} [decidable_eq α] {a : α} {l : list α} (h : list.count a l = 0) :
a l
theorem list.count_eq_zero {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
list.count a l = 0 a l
theorem list.count_eq_length {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
list.count a l = l.length ∀ (b : α), b la = b
@[simp]
theorem list.count_repeat {α : Type u_1} [decidable_eq α] (a : α) (n : ) :
theorem list.le_count_iff_repeat_sublist {α : Type u_1} [decidable_eq α] {a : α} {l : list α} {n : } :
theorem list.repeat_count_eq_of_count_eq_length {α : Type u_1} [decidable_eq α] {a : α} {l : list α} (h : list.count a l = l.length) :
@[simp]
theorem list.count_filter {α : Type u_1} [decidable_eq α] {p : α → Prop} [decidable_pred p] {a : α} {l : list α} (h : p a) :
theorem list.count_bind {α : Type u_1} {β : Type u_2} [decidable_eq β] (l : list α) (f : α → list β) (x : β) :
@[simp]
theorem list.count_map_of_injective {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (l : list α) (f : α → β) (hf : function.injective f) (x : α) :
theorem list.count_le_count_map {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (l : list α) (f : α → β) (x : α) :
@[simp]
theorem list.count_erase_self {α : Type u_1} [decidable_eq α] (a : α) (s : list α) :
@[simp]
theorem list.count_erase_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (ab : a b) (s : list α) :
theorem list.prod_map_eq_pow_single {α : Type u_1} {β : Type u_2} [decidable_eq α] [monoid β] {l : list α} (a : α) (f : α → β) (hf : ∀ (a' : α), a' aa' lf a' = 1) :
(list.map f l).prod = f a ^ list.count a l
theorem list.sum_map_eq_nsmul_single {α : Type u_1} {β : Type u_2} [decidable_eq α] [add_monoid β] {l : list α} (a : α) (f : α → β) (hf : ∀ (a' : α), a' aa' lf a' = 0) :
(list.map f l).sum = list.count a l f a
theorem list.prod_eq_pow_single {α : Type u_1} [decidable_eq α] [monoid α] {l : list α} (a : α) (h : ∀ (a' : α), a' aa' la' = 1) :
l.prod = a ^ list.count a l
theorem list.sum_eq_nsmul_single {α : Type u_1} [decidable_eq α] [add_monoid α] {l : list α} (a : α) (h : ∀ (a' : α), a' aa' la' = 0) :