# 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.

### count #

@[simp]

theorem
List.count_map_of_injective
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[DecidableEq β]
(l : List α)
(f : α → β)
(hf : Function.Injective f)
(x : α)
:

List.count (f x) (List.map f l) = List.count x l