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 Std.Data.List.Basic.
theorem
List.countP_join
{α : Type u_1}
(p : α → Bool)
(l : List (List α))
:
List.countP p (List.join l) = List.sum (List.map (List.countP p) l)
theorem
List.length_filter_lt_length_iff_exists
{α : Type u_1}
(p : α → Bool)
(l : List α)
:
List.length (List.filter p l) < List.length l ↔ ∃ (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) (List.attach l) = 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
theorem
List.count_join
{α : Type u_1}
[DecidableEq α]
(l : List (List α))
(a : α)
:
List.count a (List.join l) = List.sum (List.map (List.count a) l)
theorem
List.count_bind
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
(l : List α)
(f : α → List β)
(x : β)
:
List.count x (List.bind l f) = List.sum (List.map (List.count x ∘ f) l)
@[simp]
theorem
List.count_attach
{α : Type u_1}
{l : List α}
[DecidableEq α]
(a : { x : α // x ∈ l })
:
List.count a (List.attach l) = 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
theorem
List.sum_map_eq_nsmul_single
{α : Type u_2}
{l : List α}
[DecidableEq α]
{β : Type u_1}
[AddMonoid β]
(a : α)
(f : α → β)
(hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 0)
:
List.sum (List.map f l) = List.count a l • f a
theorem
List.prod_map_eq_pow_single
{α : Type u_2}
{l : List α}
[DecidableEq α]
{β : Type u_1}
[Monoid β]
(a : α)
(f : α → β)
(hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1)
:
List.prod (List.map f l) = f a ^ List.count a l
theorem
List.sum_eq_nsmul_single
{α : Type u_1}
{l : List α}
[DecidableEq α]
[AddMonoid α]
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ l → a' = 0)
:
List.sum l = List.count a l • a
theorem
List.prod_eq_pow_single
{α : Type u_1}
{l : List α}
[DecidableEq α]
[Monoid α]
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ l → a' = 1)
:
List.prod l = a ^ List.count a l