data.nat.count

# 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 : → Prop) (n : ) :

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

Equations
@[simp]
theorem nat.count_zero (p : → Prop)  :
0 = 0
def nat.count_set.fintype (p : → Prop) (n : ) :
fintype {i // i < n p i}

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

Equations
• = _
theorem nat.count_eq_card_filter_range (p : → Prop) (n : ) :
theorem nat.count_eq_card_fintype (p : → Prop) (n : ) :
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 : → Prop) (n : ) :
(n + 1) = n + ite (p n) 1 0
theorem nat.count_monotone (p : → Prop)  :
theorem nat.count_add (p : → Prop) (a b : ) :
(a + b) = a + nat.count (λ (k : ), p (a + k)) b
theorem nat.count_add' (p : → Prop) (a b : ) :
(a + b) = nat.count (λ (k : ), p (k + b)) a + b
theorem nat.count_one (p : → Prop)  :
1 = ite (p 0) 1 0
theorem nat.count_succ' (p : → Prop) (n : ) :
(n + 1) = nat.count (λ (k : ), p (k + 1)) n + ite (p 0) 1 0
@[simp]
theorem nat.count_lt_count_succ_iff {p : → Prop} {n : } :
n < (n + 1) p n
theorem nat.count_succ_eq_succ_count_iff {p : → Prop} {n : } :
(n + 1) = n + 1 p n
theorem nat.count_succ_eq_count_iff {p : → Prop} {n : } :
(n + 1) = n ¬p n
theorem nat.count_succ_eq_succ_count {p : → Prop} {n : } :
p n (n + 1) = n + 1

Alias of the reverse direction of nat.count_succ_eq_succ_count_iff.

theorem nat.count_succ_eq_count {p : → Prop} {n : } :
¬p n (n + 1) = n

Alias of the reverse direction of nat.count_succ_eq_count_iff.

theorem nat.count_le_cardinal {p : → Prop} (n : ) :
n) cardinal.mk {k : | p k}
theorem nat.lt_of_count_lt_count {p : → Prop} {a b : } (h : a < b) :
a < b
theorem nat.count_strict_mono {p : → Prop} {m n : } (hm : p m) (hmn : m < n) :
m < n
theorem nat.count_injective {p : → Prop} {m n : } (hm : p m) (hn : p n) (heq : m = n) :
m = n
theorem nat.count_le_card {p : → Prop} (hp : (set_of p).finite) (n : ) :
theorem nat.count_lt_card {p : → Prop} {n : } (hp : (set_of p).finite) (hpn : p n) :
theorem nat.count_mono_left {p : → Prop} {q : → Prop} {n : } (hpq : ∀ (k : ), p kq k) :
n n