mathlib documentation

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) [decidable_pred p] (n : ) :

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

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

Alias of count_succ_eq_succ_count_iff.

theorem count_succ_eq_count {p : → Prop} [decidable_pred p] {n : } :
¬p nnat.count p (n + 1) = nat.count p n

Alias of count_succ_eq_count_iff.

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