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.

@[simp]

theorem List.countP_lt_length_iff {α : Type u_1} {l : List α} {p : α → Bool} : countP p l < l.length ↔ ∃ (a : α), a ∈ l ∧ p a = false

@[simp]

theorem List.count_lt_length_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : count a l < l.length ↔ ∃ (b : α), b ∈ l ∧ b ≠ a

theorem List.countP_erase {α : Type u_1} [BEq α] [LawfulBEq α] (p : α → Bool) (l : List α) (a : α) : countP p (l.erase a) = countP p l - if a ∈ l ∧ p a = true then 1 else 0

theorem List.count_diff {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l₁ l₂ : List α) : count a (l₁.diff l₂) = count a l₁ - count a l₂

theorem List.countP_diff {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} (hl : l₂.Subperm l₁) (p : α → Bool) : countP p (l₁.diff l₂) = countP p l₁ - countP p l₂

@[simp]

theorem List.count_map_of_injective {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] (l : List α) (f : α → β) (hf : Function.Injective f) (x : α) : count (f x) (map f l) = count x l