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 : α) : List.count (f x) (List.map f l) = List.count x l