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.
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
@[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