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