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)  :
@[simp]
theorem list.countp_cons_of_pos {α : Type u_1} (p : α → Prop) {a : α} (l : list α) (pa : p a) :
(a :: l) = l + 1
@[simp]
theorem list.countp_cons_of_neg {α : Type u_1} (p : α → Prop) {a : α} (l : list α) (pa : ¬p a) :
(a :: l) = l
theorem list.countp_cons {α : Type u_1} (p : α → Prop) (a : α) (l : list α) :
(a :: l) = l + ite (p a) 1 0
theorem list.length_eq_countp_add_countp {α : Type u_1} (p : α → Prop) (l : list α) :
l.length = l + list.countp (λ (a : α), ¬p a) l
theorem list.countp_eq_length_filter {α : Type u_1} (p : α → Prop) (l : list α) :
l = l).length
theorem list.countp_le_length {α : Type u_1} {l : list α} (p : α → Prop)  :
l l.length
@[simp]
theorem list.countp_append {α : Type u_1} (p : α → Prop) (l₁ l₂ : list α) :
(l₁ ++ l₂) = l₁ + l₂
theorem list.countp_pos {α : Type u_1} (p : α → Prop) {l : list α} :
0 < l ∃ (a : α) (H : a l), p a
theorem list.countp_eq_zero {α : Type u_1} (p : α → Prop) {l : list α} :
l = 0 ∀ (a : α), a l¬p a
theorem list.countp_eq_length {α : Type u_1} (p : α → Prop) {l : list α} :
l = l.length ∀ (a : α), a lp a
theorem list.length_filter_lt_length_iff_exists {α : Type u_1} (p : α → Prop) (l : list α) :
l).length < l.length ∃ (x : α) (H : x l), ¬p x
theorem list.sublist.countp_le {α : Type u_1} {l₁ l₂ : list α} (p : α → Prop) (s : l₁ <+ l₂) :
l₁ l₂
@[simp]
theorem list.countp_filter {α : Type u_1} (p : α → Prop) {q : α → Prop} (l : list α) :
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 α) :
(b :: l) = ite (a = b) l).succ l)
theorem list.count_cons' {α : Type u_1} [decidable_eq α] (a b : α) (l : list α) :
(b :: l) = l + ite (a = b) 1 0
@[simp]
theorem list.count_cons_self {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
(a :: l) = l).succ
@[simp]
theorem list.count_cons_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (h : a b) (l : list α) :
(b :: l) = l
theorem list.count_tail {α : Type u_1} [decidable_eq α] (l : list α) (a : α) (h : 0 < l.length) :
l.tail = l - ite (a = l.nth_le 0 h) 1 0
theorem list.count_le_length {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
l l.length
theorem list.sublist.count_le {α : Type u_1} {l₁ l₂ : list α} [decidable_eq α] (h : l₁ <+ l₂) (a : α) :
l₁ l₂
theorem list.count_le_count_cons {α : Type u_1} [decidable_eq α] (a b : α) (l : list α) :
l (b :: l)
theorem list.count_singleton {α : Type u_1} [decidable_eq α] (a : α) :
[a] = 1
theorem list.count_singleton' {α : Type u_1} [decidable_eq α] (a b : α) :
[b] = ite (a = b) 1 0
@[simp]
theorem list.count_append {α : Type u_1} [decidable_eq α] (a : α) (l₁ l₂ : list α) :
(l₁ ++ l₂) = l₁ + l₂
theorem list.count_concat {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
(l.concat a) = l).succ
@[simp]
theorem list.count_pos {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
0 < l a l
@[simp]
theorem list.one_le_count_iff_mem {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
1 l a l
@[simp]
theorem list.count_eq_zero_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {l : list α} (h : a l) :
l = 0
theorem list.not_mem_of_count_eq_zero {α : Type u_1} [decidable_eq α] {a : α} {l : list α} (h : l = 0) :
a l
theorem list.count_eq_zero {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
l = 0 a l
theorem list.count_eq_length {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
l = l.length ∀ (b : α), b la = b
@[simp]
theorem list.count_repeat {α : Type u_1} [decidable_eq α] (a : α) (n : ) :
n) = n
theorem list.le_count_iff_repeat_sublist {α : Type u_1} [decidable_eq α] {a : α} {l : list α} {n : } :
n l n <+ l
theorem list.repeat_count_eq_of_count_eq_length {α : Type u_1} [decidable_eq α] {a : α} {l : list α} (h : l = l.length) :
l) = l
@[simp]
theorem list.count_filter {α : Type u_1} [decidable_eq α] {p : α → Prop} {a : α} {l : list α} (h : p a) :
l) = l
theorem list.count_bind {α : Type u_1} {β : Type u_2} [decidable_eq β] (l : list α) (f : α → list β) (x : β) :
(l.bind f) = (list.map f) l).sum
@[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 : α) :
list.count (f x) (list.map f l) = l
theorem list.count_le_count_map {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (l : list α) (f : α → β) (x : α) :
l list.count (f x) (list.map f l)
@[simp]
theorem list.count_erase_self {α : Type u_1} [decidable_eq α] (a : α) (s : list α) :
(s.erase a) = s).pred
@[simp]
theorem list.count_erase_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (ab : a b) (s : list α) :
(s.erase b) = s
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 ^ 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 = 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 ^ l
theorem list.sum_eq_nsmul_single {α : Type u_1} [decidable_eq α] [add_monoid α] {l : list α} (a : α) (h : ∀ (a' : α), a' aa' la' = 0) :
l.sum = l a