mathlib3 documentation

data.nat.count

Counting on ℕ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

nat.count p n = list.countp p (list.range n)

@[simp]

theorem nat.count_zero (p : ℕ → Prop) [decidable_pred p] :

nat.count p 0 = 0

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

nat.count_set.fintype p n = fintype.of_finset (finset.filter p (finset.range n)) _

theorem nat.count_eq_card_filter_range (p : ℕ → Prop) [decidable_pred p] (n : ℕ) :

nat.count p n = (finset.filter p (finset.range n)).card

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] :

monotone (nat.count 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 nat.count_succ_eq_succ_count {p : ℕ → Prop} [decidable_pred p] {n : ℕ} :

p n → nat.count p (n + 1) = nat.count p n + 1

Alias of the reverse direction of nat.count_succ_eq_succ_count_iff.

theorem nat.count_succ_eq_count {p : ℕ → Prop} [decidable_pred p] {n : ℕ} :

¬p n → nat.count p (n + 1) = nat.count p n

Alias of the reverse direction of nat.count_succ_eq_count_iff.

theorem nat.count_le_cardinal {p : ℕ → Prop} [decidable_pred p] (n : ℕ) :

↑(nat.count p n) ≤ cardinal.mk ↥{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) :

nat.count p m < nat.count p 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 : ℕ) :

nat.count p n ≤ hp.to_finset.card

theorem nat.count_lt_card {p : ℕ → Prop} [decidable_pred p] {n : ℕ} (hp : (set_of p).finite) (hpn : p n) :

nat.count p n < hp.to_finset.card

theorem nat.count_mono_left {p : ℕ → Prop} [decidable_pred p] {q : ℕ → Prop} [decidable_pred q] {n : ℕ} (hpq : ∀ (k : ℕ), p k → q k) :

nat.count p n ≤ nat.count q n