# Documentation

Mathlib.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 Std.Data.List.Basic.

@[simp]
theorem List.countp_nil {α : Type u_1} (p : αBool) :
List.countp p [] = 0
theorem List.countp_go_eq_add {α : Type u_1} (p : αBool) {n : } (l : List α) :
= n +
@[simp]
theorem List.countp_cons_of_pos {α : Type u_1} (p : αBool) {a : α} (l : List α) (pa : p a = true) :
List.countp p (a :: l) = + 1
@[simp]
theorem List.countp_cons_of_neg {α : Type u_1} (p : αBool) {a : α} (l : List α) (pa : ¬p a = true) :
List.countp p (a :: l) =
theorem List.countp_cons {α : Type u_1} (p : αBool) (a : α) (l : List α) :
List.countp p (a :: l) = + if p a = true then 1 else 0
theorem List.length_eq_countp_add_countp {α : Type u_1} (p : αBool) (l : List α) :
= + List.countp (fun a => decide ¬p a = true) l
theorem List.countp_eq_length_filter {α : Type u_1} (p : αBool) (l : List α) :
theorem List.countp_le_length {α : Type u_1} {l : List α} (p : αBool) :
@[simp]
theorem List.countp_append {α : Type u_1} (p : αBool) (l₁ : List α) (l₂ : List α) :
List.countp p (l₁ ++ l₂) = List.countp p l₁ + List.countp p l₂
theorem List.countp_join {α : Type u_1} (p : αBool) (l : List (List α)) :
theorem List.countp_pos {α : Type u_1} {l : List α} (p : αBool) :
0 < a, a l p a = true
@[simp]
theorem List.countp_eq_zero {α : Type u_1} {l : List α} (p : αBool) :
= 0 ∀ (a : α), a l¬p a = true
@[simp]
theorem List.countp_eq_length {α : Type u_1} {l : List α} (p : αBool) :
= ∀ (a : α), a lp a = true
theorem List.length_filter_lt_length_iff_exists {α : Type u_1} (p : αBool) (l : List α) :
List.length () < x, x l ¬p x = true
theorem List.Sublist.countp_le {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : List.Sublist l₁ l₂) :
@[simp]
theorem List.countp_filter {α : Type u_1} (p : αBool) (q : αBool) (l : List α) :
List.countp p () = List.countp (fun a => decide (p a = true q a = true)) l
@[simp]
theorem List.countp_true {α : Type u_1} {l : List α} :
List.countp (fun x => true) l =
@[simp]
theorem List.countp_false {α : Type u_1} {l : List α} :
List.countp (fun x => false) l = 0
@[simp]
theorem List.countp_map {α : Type u_2} {β : Type u_1} (p : βBool) (f : αβ) (l : List α) :
theorem List.countp_mono_left {α : Type u_1} {l : List α} {p : αBool} {q : αBool} (h : ∀ (x : α), x lp x = trueq x = true) :
theorem List.countp_congr {α : Type u_1} {l : List α} {p : αBool} {q : αBool} (h : ∀ (x : α), x l → (p x = true q x = true)) :
=

### count #

@[simp]
theorem List.count_nil {α : Type u_1} [inst : ] (a : α) :
List.count a [] = 0
theorem List.count_cons' {α : Type u_1} [inst : ] (a : α) (b : α) (l : List α) :
List.count a (b :: l) = + if a = b then 1 else 0
theorem List.count_cons {α : Type u_1} [inst : ] (a : α) (b : α) (l : List α) :
List.count a (b :: l) = if a = b then Nat.succ () else
@[simp]
theorem List.count_cons_self {α : Type u_1} [inst : ] (a : α) (l : List α) :
List.count a (a :: l) = + 1
@[simp]
theorem List.count_cons_of_ne {α : Type u_1} [inst : ] {a : α} {b : α} (h : a b) (l : List α) :
List.count a (b :: l) =
theorem List.count_tail {α : Type u_1} [inst : ] (l : List α) (a : α) (h : 0 < ) :
List.count a () = - if a = List.get l { val := 0, isLt := h } then 1 else 0
theorem List.count_le_length {α : Type u_1} [inst : ] (a : α) (l : List α) :
theorem List.Sublist.count_le {α : Type u_1} [inst : ] {l₁ : List α} {l₂ : List α} (h : List.Sublist l₁ l₂) (a : α) :
List.count a l₁ List.count a l₂
theorem List.count_le_count_cons {α : Type u_1} [inst : ] (a : α) (b : α) (l : List α) :
List.count a (b :: l)
theorem List.count_singleton {α : Type u_1} [inst : ] (a : α) :
List.count a [a] = 1
theorem List.count_singleton' {α : Type u_1} [inst : ] (a : α) (b : α) :
List.count a [b] = if a = b then 1 else 0
@[simp]
theorem List.count_append {α : Type u_1} [inst : ] (a : α) (l₁ : List α) (l₂ : List α) :
List.count a (l₁ ++ l₂) = List.count a l₁ + List.count a l₂
theorem List.count_join {α : Type u_1} [inst : ] (l : List (List α)) (a : α) :
theorem List.count_concat {α : Type u_1} [inst : ] (a : α) (l : List α) :
@[simp]
theorem List.count_pos {α : Type u_1} [inst : ] {a : α} {l : List α} :
0 < a l
@[simp]
theorem List.one_le_count_iff_mem {α : Type u_1} [inst : ] {a : α} {l : List α} :
1 a l
@[simp]
theorem List.count_eq_zero_of_not_mem {α : Type u_1} [inst : ] {a : α} {l : List α} (h : ¬a l) :
= 0
theorem List.not_mem_of_count_eq_zero {α : Type u_1} [inst : ] {a : α} {l : List α} (h : = 0) :
¬a l
@[simp]
theorem List.count_eq_zero {α : Type u_1} {l : List α} [inst : ] {a : α} :
= 0 ¬a l
@[simp]
theorem List.count_eq_length {α : Type u_1} {l : List α} [inst : ] {a : α} :
= ∀ (b : α), b la = b
@[simp]
theorem List.count_replicate_self {α : Type u_1} [inst : ] (a : α) (n : ) :
List.count a () = n
theorem List.count_replicate {α : Type u_1} [inst : ] (a : α) (b : α) (n : ) :
List.count a () = if a = b then n else 0
theorem List.filter_beq' {α : Type u_1} [inst : ] (l : List α) (a : α) :
List.filter (fun x => x == a) l = List.replicate () a
theorem List.filter_eq' {α : Type u_1} [inst : ] (l : List α) (a : α) :
List.filter (fun x => decide (x = a)) l = List.replicate () a
theorem List.filter_eq {α : Type u_1} [inst : ] (l : List α) (a : α) :
List.filter (fun x => decide (a = x)) l = List.replicate () a
theorem List.filter_beq {α : Type u_1} [inst : ] (l : List α) (a : α) :
List.filter (fun x => a == x) l = List.replicate () a
theorem List.le_count_iff_replicate_sublist {α : Type u_1} {l : List α} [inst : ] {n : } {a : α} :
theorem List.replicate_count_eq_of_count_eq_length {α : Type u_1} {l : List α} [inst : ] {a : α} (h : = ) :
@[simp]
theorem List.count_filter {α : Type u_1} {l : List α} [inst : ] {p : αBool} {a : α} (h : p a = true) :
theorem List.count_bind {α : Type u_1} {β : Type u_2} [inst : ] (l : List α) (f : αList β) (x : β) :
@[simp]
theorem List.count_map_of_injective {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (l : List α) (f : αβ) (hf : ) (x : α) :
List.count (f x) (List.map f l) =
theorem List.count_le_count_map {α : Type u_2} [inst : ] {β : Type u_1} [inst : ] (l : List α) (f : αβ) (x : α) :
List.count (f x) (List.map f l)
theorem List.count_erase {α : Type u_1} [inst : ] (a : α) (b : α) (l : List α) :
List.count a () = - if a = b then 1 else 0
@[simp]
theorem List.count_erase_self {α : Type u_1} [inst : ] (a : α) (l : List α) :
List.count a () = - 1
@[simp]
theorem List.count_erase_of_ne {α : Type u_1} [inst : ] {a : α} {b : α} (ab : a b) (l : List α) :
theorem List.sum_map_eq_nsmul_single {α : Type u_2} {l : List α} [inst : ] {β : Type u_1} [inst : ] (a : α) (f : αβ) (hf : ∀ (a' : α), a' aa' lf a' = 0) :
theorem List.prod_map_eq_pow_single {α : Type u_2} {l : List α} [inst : ] {β : Type u_1} [inst : ] (a : α) (f : αβ) (hf : ∀ (a' : α), a' aa' lf a' = 1) :
List.prod (List.map f l) = f a ^
theorem List.sum_eq_nsmul_single {α : Type u_1} {l : List α} [inst : ] [inst : ] (a : α) (h : ∀ (a' : α), a' aa' la' = 0) :
= a
theorem List.prod_eq_pow_single {α : Type u_1} {l : List α} [inst : ] [inst : ] (a : α) (h : ∀ (a' : α), a' aa' la' = 1) :
= a ^