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

theorem List.length_filter_lt_length_iff_exists {α : Type u_1} (p : αBool) (l : List α) :
(List.filter p l).length < l.length ∃ (x : α), x l ¬p x = true
theorem List.countP_attach {α : Type u_1} (p : αBool) (l : List α) :
List.countP (fun (a : { x : α // x l }) => p a) l.attach = List.countP p l

count #

@[deprecated]
theorem List.count_cons' {α : Type u_1} [DecidableEq α] (a : α) (b : α) (l : List α) :
List.count a (b :: l) = List.count a l + if a = b then 1 else 0
@[simp]
theorem List.count_attach {α : Type u_1} {l : List α} [DecidableEq α] (a : { x : α // x l }) :
List.count a l.attach = List.count (a) l
@[simp]
theorem List.count_map_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (l : List α) (f : αβ) (hf : Function.Injective f) (x : α) :