mathlib documentation

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) [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_join {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list (list α)) :
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
@[simp]
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
@[simp]
theorem list.countp_eq_length {α : Type u_1} (p : α Prop) [decidable_pred p] {l : list α} :
list.countp p l = l.length (a : α), a l p 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 q : α Prop) [decidable_pred p] [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
@[simp]
theorem list.countp_map {α : Type u_1} {β : Type u_2} (p : β Prop) [decidable_pred p] (f : α β) (l : list α) :
theorem list.countp_mono_left {α : Type u_1} {l : list α} {p q : α Prop} [decidable_pred p] [decidable_pred q] (h : (x : α), x l p x q x) :
theorem list.countp_congr {α : Type u_1} {l : list α} {p q : α Prop} [decidable_pred p] [decidable_pred q] (h : (x : α), x l (p x q x)) :

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 + 1
@[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_join {α : Type u_1} [decidable_eq α] (l : list (list α)) (a : α) :
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
@[simp]
theorem list.count_eq_zero {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
list.count a l = 0 a l
@[simp]
theorem list.count_eq_length {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :
list.count a l = l.length (b : α), b l a = b
@[simp]
theorem list.count_replicate_self {α : Type u_1} [decidable_eq α] (a : α) (n : ) :
theorem list.count_replicate {α : Type u_1} [decidable_eq α] (a b : α) (n : ) :
list.count a (list.replicate 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 (list.count a l) a
theorem list.le_count_iff_replicate_sublist {α : Type u_1} [decidable_eq α] {a : α} {l : list α} {n : } :
theorem list.replicate_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 : α) :
theorem list.count_erase {α : Type u_1} [decidable_eq α] (a b : α) (l : list α) :
list.count a (l.erase b) = list.count a l - ite (a = b) 1 0
@[simp]
theorem list.count_erase_self {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
list.count a (l.erase a) = list.count a l - 1
@[simp]
theorem list.count_erase_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (ab : a b) (l : list α) :
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 ^ 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' a a' l f 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' a a' l a' = 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' a a' l a' = 0) :