Counting in lists #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 data.list.defs.
@[simp]
theorem
list.countp_nil
{α : Type u_1}
(p : α → Prop)
[decidable_pred p] :
list.countp p list.nil = 0
@[simp]
theorem
list.countp_cons_of_pos
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
{a : α}
(l : list α)
(pa : p a) :
list.countp p (a :: l) = list.countp p l + 1
@[simp]
theorem
list.countp_cons_of_neg
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
{a : α}
(l : list α)
(pa : ¬p a) :
list.countp p (a :: l) = list.countp p l
theorem
list.countp_cons
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(a : α)
(l : list α) :
list.countp p (a :: l) = list.countp p l + ite (p a) 1 0
theorem
list.length_eq_countp_add_countp
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
l.length = list.countp p l + list.countp (λ (a : α), ¬p a) l
theorem
list.countp_eq_length_filter
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.countp p l = (list.filter p l).length
theorem
list.countp_le_length
{α : Type u_1}
{l : list α}
(p : α → Prop)
[decidable_pred p] :
list.countp p l ≤ l.length
@[simp]
theorem
list.countp_append
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l₁ l₂ : list α) :
list.countp p (l₁ ++ l₂) = list.countp p l₁ + list.countp p l₂
theorem
list.countp_join
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list (list α)) :
list.countp p l.join = (list.map (list.countp p) l).sum
@[simp]
@[simp]
theorem
list.length_filter_lt_length_iff_exists
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
theorem
list.sublist.countp_le
{α : Type u_1}
{l₁ l₂ : list α}
(p : α → Prop)
[decidable_pred p]
(s : l₁ <+ l₂) :
list.countp p l₁ ≤ list.countp p l₂
@[simp]
theorem
list.countp_filter
{α : Type u_1}
(p q : α → Prop)
[decidable_pred p]
[decidable_pred q]
(l : list α) :
list.countp p (list.filter q l) = list.countp (λ (a : α), p a ∧ q a) l
@[simp]
@[simp]
@[simp]
theorem
list.countp_map
{α : Type u_1}
{β : Type u_2}
(p : β → Prop)
[decidable_pred p]
(f : α → β)
(l : list α) :
list.countp p (list.map f l) = list.countp (p ∘ f) l
@[simp]
theorem
list.countp_attach
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.countp (λ (a : {x // x ∈ l}), p ↑a) l.attach = list.countp p l
theorem
list.countp_mono_left
{α : Type u_1}
{l : list α}
{p q : α → Prop}
[decidable_pred p]
[decidable_pred q]
(h : ∀ (x : α), x ∈ l → p x → q x) :
list.countp p l ≤ list.countp q l
theorem
list.countp_congr
{α : Type u_1}
{l : list α}
{p q : α → Prop}
[decidable_pred p]
[decidable_pred q]
(h : ∀ (x : α), x ∈ l → (p x ↔ q x)) :
list.countp p l = list.countp q l
count #
@[simp]
theorem
list.count_cons
{α : Type u_1}
[decidable_eq α]
(a b : α)
(l : list α) :
list.count a (b :: l) = ite (a = b) (list.count a l).succ (list.count a l)
theorem
list.count_cons'
{α : Type u_1}
[decidable_eq α]
(a b : α)
(l : list α) :
list.count a (b :: l) = list.count a l + ite (a = b) 1 0
@[simp]
theorem
list.count_cons_self
{α : Type u_1}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a (a :: l) = list.count a l + 1
@[simp]
theorem
list.count_cons_of_ne
{α : Type u_1}
[decidable_eq α]
{a b : α}
(h : a ≠ b)
(l : list α) :
list.count a (b :: l) = list.count a l
theorem
list.count_tail
{α : Type u_1}
[decidable_eq α]
(l : list α)
(a : α)
(h : 0 < l.length) :
list.count a l.tail = list.count a l - ite (a = l.nth_le 0 h) 1 0
theorem
list.count_le_length
{α : Type u_1}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a l ≤ l.length
theorem
list.sublist.count_le
{α : Type u_1}
{l₁ l₂ : list α}
[decidable_eq α]
(h : l₁ <+ l₂)
(a : α) :
list.count a l₁ ≤ list.count a l₂
theorem
list.count_le_count_cons
{α : Type u_1}
[decidable_eq α]
(a b : α)
(l : list α) :
list.count a l ≤ list.count a (b :: l)
theorem
list.count_singleton'
{α : Type u_1}
[decidable_eq α]
(a b : α) :
list.count a [b] = ite (a = b) 1 0
@[simp]
theorem
list.count_append
{α : Type u_1}
[decidable_eq α]
(a : α)
(l₁ l₂ : list α) :
list.count a (l₁ ++ l₂) = list.count a l₁ + list.count a l₂
theorem
list.count_join
{α : Type u_1}
[decidable_eq α]
(l : list (list α))
(a : α) :
list.count a l.join = (list.map (list.count a) l).sum
theorem
list.count_concat
{α : Type u_1}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a (l.concat a) = (list.count a l).succ
@[simp]
theorem
list.count_pos
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α} :
0 < list.count a l ↔ a ∈ l
@[simp]
theorem
list.one_le_count_iff_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α} :
1 ≤ list.count a l ↔ a ∈ l
@[simp]
theorem
list.count_eq_zero_of_not_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α}
(h : a ∉ l) :
list.count a l = 0
theorem
list.not_mem_of_count_eq_zero
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α}
(h : list.count a l = 0) :
a ∉ l
@[simp]
theorem
list.count_eq_zero
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α} :
list.count a l = 0 ↔ a ∉ l
@[simp]
@[simp]
theorem
list.count_replicate_self
{α : Type u_1}
[decidable_eq α]
(a : α)
(n : ℕ) :
list.count a (list.replicate n a) = n
theorem
list.count_replicate
{α : Type u_1}
[decidable_eq α]
(a b : α)
(n : ℕ) :
list.count a (list.replicate n b) = ite (a = b) n 0
theorem
list.filter_eq
{α : Type u_1}
[decidable_eq α]
(l : list α)
(a : α) :
list.filter (eq a) l = list.replicate (list.count a l) a
theorem
list.filter_eq'
{α : Type u_1}
[decidable_eq α]
(l : list α)
(a : α) :
list.filter (λ (x : α), x = a) l = list.replicate (list.count a l) a
theorem
list.le_count_iff_replicate_sublist
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α}
{n : ℕ} :
n ≤ list.count a l ↔ list.replicate n a <+ l
theorem
list.replicate_count_eq_of_count_eq_length
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α}
(h : list.count a l = l.length) :
list.replicate (list.count a l) a = l
@[simp]
theorem
list.count_filter
{α : Type u_1}
[decidable_eq α]
{p : α → Prop}
[decidable_pred p]
{a : α}
{l : list α}
(h : p a) :
list.count a (list.filter p l) = list.count a l
theorem
list.count_bind
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
(l : list α)
(f : α → list β)
(x : β) :
list.count x (l.bind f) = (list.map (list.count x ∘ f) l).sum
@[simp]
theorem
list.count_attach
{α : Type u_1}
{l : list α}
[decidable_eq α]
(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}
[decidable_eq α]
[decidable_eq β]
(l : list α)
(f : α → β)
(hf : function.injective f)
(x : α) :
list.count (f x) (list.map f l) = list.count x l
theorem
list.count_le_count_map
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
(l : list α)
(f : α → β)
(x : α) :
list.count x l ≤ list.count (f x) (list.map f l)
theorem
list.count_erase
{α : Type u_1}
[decidable_eq α]
(a b : α)
(l : list α) :
list.count a (l.erase b) = list.count a l - ite (a = b) 1 0
@[simp]
theorem
list.count_erase_self
{α : Type u_1}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a (l.erase a) = list.count a l - 1
@[simp]
theorem
list.count_erase_of_ne
{α : Type u_1}
[decidable_eq α]
{a b : α}
(ab : a ≠ b)
(l : list α) :
list.count a (l.erase b) = list.count a l
theorem
list.sum_map_eq_nsmul_single
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[add_monoid β]
{l : list α}
(a : α)
(f : α → β)
(hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 0) :
(list.map f l).sum = list.count a l • f a
theorem
list.sum_eq_nsmul_single
{α : Type u_1}
[decidable_eq α]
[add_monoid α]
{l : list α}
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ l → a' = 0) :
l.sum = list.count a l • a