# Counting on ℕ #

This file defines the count function, which gives, for any predicate on the natural numbers, "how many numbers under k satisfy this predicate?". We then prove several expected lemmas about count, relating it to the cardinality of other objects, and helping to evaluate it for specific k.

def Nat.count (p : ) [] (n : ) :

Count the number of naturals k < n satisfying p k.

Equations
Instances For
@[simp]
theorem Nat.count_zero (p : ) [] :
= 0
def Nat.CountSet.fintype (p : ) [] (n : ) :
Fintype { i : // i < n p i }

A fintype instance for the set relevant to Nat.count. Locally an instance in locale count

Equations
Instances For
theorem Nat.count_eq_card_filter_range (p : ) [] (n : ) :
= ().card
theorem Nat.count_eq_card_fintype (p : ) [] (n : ) :
= Fintype.card { k : // k < n p k }

count p n can be expressed as the cardinality of {k // k < n ∧ p k}.

theorem Nat.count_succ (p : ) [] (n : ) :
Nat.count p (n + 1) = + if p n then 1 else 0
theorem Nat.count_monotone (p : ) [] :
theorem Nat.count_add (p : ) [] (a : ) (b : ) :
Nat.count p (a + b) = + Nat.count (fun (k : ) => p (a + k)) b
theorem Nat.count_add' (p : ) [] (a : ) (b : ) :
Nat.count p (a + b) = Nat.count (fun (k : ) => p (k + b)) a +
theorem Nat.count_one (p : ) [] :
= if p 0 then 1 else 0
theorem Nat.count_succ' (p : ) [] (n : ) :
Nat.count p (n + 1) = Nat.count (fun (k : ) => p (k + 1)) n + if p 0 then 1 else 0
@[simp]
theorem Nat.count_lt_count_succ_iff {p : } [] {n : } :
< Nat.count p (n + 1) p n
theorem Nat.count_succ_eq_succ_count_iff {p : } [] {n : } :
Nat.count p (n + 1) = + 1 p n
theorem Nat.count_succ_eq_count_iff {p : } [] {n : } :
Nat.count p (n + 1) = ¬p n
theorem Nat.count_succ_eq_succ_count {p : } [] {n : } :
p nNat.count p (n + 1) = + 1

Alias of the reverse direction of Nat.count_succ_eq_succ_count_iff.

theorem Nat.count_succ_eq_count {p : } [] {n : } :
¬p nNat.count p (n + 1) =

Alias of the reverse direction of Nat.count_succ_eq_count_iff.

theorem Nat.count_le_cardinal {p : } [] (n : ) :
() Cardinal.mk {k : | p k}
theorem Nat.lt_of_count_lt_count {p : } [] {a : } {b : } (h : < ) :
a < b
theorem Nat.count_strict_mono {p : } [] {m : } {n : } (hm : p m) (hmn : m < n) :
<
theorem Nat.count_injective {p : } [] {m : } {n : } (hm : p m) (hn : p n) (heq : = ) :
m = n
theorem Nat.count_le_card {p : } [] (hp : ().Finite) (n : ) :
hp.toFinset.card
theorem Nat.count_lt_card {p : } [] {n : } (hp : ().Finite) (hpn : p n) :
< hp.toFinset.card
theorem Nat.count_of_forall {p : } [] {n : } (hp : n' < n, p n') :
= n
@[simp]
theorem Nat.count_true (n : ) :
Nat.count (fun (x : ) => True) n = n
theorem Nat.count_of_forall_not {p : } [] {n : } (hp : n' < n, ¬p n') :
= 0
@[simp]
theorem Nat.count_false (n : ) :
Nat.count (fun (x : ) => False) n = 0
theorem Nat.count_mono_left {p : } [] {q : } [] {n : } (hpq : ∀ (k : ), p kq k) :