data.list.count

# Counting in lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_join {α : Type u_1} (p : α Prop) (l : list (list α)) :
theorem list.countp_pos {α : Type u_1} (p : α Prop) {l : list α} :
0 < l (a : α) (H : a l), p a
@[simp]
theorem list.countp_eq_zero {α : Type u_1} (p : α Prop) {l : list α} :
l = 0 (a : α), a l ¬p a
@[simp]
theorem list.countp_eq_length {α : Type u_1} (p : α Prop) {l : list α} :
l = l.length (a : α), a l p 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 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
@[simp]
theorem list.countp_map {α : Type u_1} {β : Type u_2} (p : β Prop) (f : α β) (l : list α) :
(list.map f l) = list.countp (p f) l
@[simp]
theorem list.countp_attach {α : Type u_1} (p : α Prop) (l : list α) :
list.countp (λ (a : {x // x l}), p a) l.attach = l
theorem list.countp_mono_left {α : Type u_1} {l : list α} {p q : α Prop} (h : (x : α), x l p x q x) :
l l
theorem list.countp_congr {α : Type u_1} {l : list α} {p q : α Prop} (h : (x : α), x l (p x q x)) :
l = l

### 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 + 1
@[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_join {α : Type u_1} [decidable_eq α] (l : list (list α)) (a : α) :
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
@[simp]
theorem list.count_eq_zero {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
l = 0 a l
@[simp]
theorem list.count_eq_length {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
l = l.length (b : α), b l a = b
@[simp]
theorem list.count_replicate_self {α : Type u_1} [decidable_eq α] (a : α) (n : ) :
a) = n
theorem list.count_replicate {α : Type u_1} [decidable_eq α] (a b : α) (n : ) :
b) = ite (a = b) n 0
theorem list.filter_eq {α : Type u_1} [decidable_eq α] (l : list α) (a : α) :
theorem list.filter_eq' {α : Type u_1} [decidable_eq α] (l : list α) (a : α) :
list.filter (λ (x : α), x = a) l = list.replicate l) a
theorem list.le_count_iff_replicate_sublist {α : Type u_1} [decidable_eq α] {a : α} {l : list α} {n : } :
n l <+ l
theorem list.replicate_count_eq_of_count_eq_length {α : Type u_1} [decidable_eq α] {a : α} {l : list α} (h : l = l.length) :
@[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_attach {α : Type u_1} {l : list α} [decidable_eq α] (a : {x // x l}) :
l.attach = l
@[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)
theorem list.count_erase {α : Type u_1} [decidable_eq α] (a b : α) (l : list α) :
(l.erase b) = l - ite (a = b) 1 0
@[simp]
theorem list.count_erase_self {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
(l.erase a) = l - 1
@[simp]
theorem list.count_erase_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (ab : a b) (l : list α) :
(l.erase b) = l
theorem list.prod_map_eq_pow_single {α : Type u_1} {β : Type u_2} [decidable_eq α] [monoid β] {l : list α} (a : α) (f : α β) (hf : (a' : α), a' a a' l f 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' a a' l f 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' a a' l a' = 1) :
l.prod = a ^ l
theorem list.sum_eq_nsmul_single {α : Type u_1} [decidable_eq α] [add_monoid α] {l : list α} (a : α) (h : (a' : α), a' a a' l a' = 0) :
l.sum = l a