Documentation

Mathlib.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) [DecidablePred p] (n : ) :

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

Equations
Instances For
    @[simp]
    theorem Nat.count_zero (p : Prop) [DecidablePred p] :
    Nat.count p 0 = 0
    def Nat.CountSet.fintype (p : Prop) [DecidablePred 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_fintype (p : Prop) [DecidablePred 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) [DecidablePred p] (n : ) :
      Nat.count p (n + 1) = Nat.count p n + if p n then 1 else 0
      theorem Nat.count_add (p : Prop) [DecidablePred p] (a : ) (b : ) :
      Nat.count p (a + b) = Nat.count p a + Nat.count (fun (k : ) => p (a + k)) b
      theorem Nat.count_add' (p : Prop) [DecidablePred p] (a : ) (b : ) :
      Nat.count p (a + b) = Nat.count (fun (k : ) => p (k + b)) a + Nat.count p b
      theorem Nat.count_one (p : Prop) [DecidablePred p] :
      Nat.count p 1 = if p 0 then 1 else 0
      theorem Nat.count_succ' (p : Prop) [DecidablePred 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 : Prop} [DecidablePred p] {n : } :
      Nat.count p n < Nat.count p (n + 1) p n
      theorem Nat.count_succ_eq_succ_count_iff {p : Prop} [DecidablePred p] {n : } :
      Nat.count p (n + 1) = Nat.count p n + 1 p n
      theorem Nat.count_succ_eq_count_iff {p : Prop} [DecidablePred p] {n : } :
      Nat.count p (n + 1) = Nat.count p n ¬p n
      theorem Nat.count_succ_eq_succ_count {p : Prop} [DecidablePred p] {n : } :
      p nNat.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} [DecidablePred p] {n : } :
      ¬p nNat.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} [DecidablePred p] (n : ) :
      (Nat.count p n) Cardinal.mk {k : | p k}
      theorem Nat.lt_of_count_lt_count {p : Prop} [DecidablePred p] {a : } {b : } (h : Nat.count p a < Nat.count p b) :
      a < b
      theorem Nat.count_strict_mono {p : Prop} [DecidablePred p] {m : } {n : } (hm : p m) (hmn : m < n) :
      theorem Nat.count_injective {p : Prop} [DecidablePred 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} [DecidablePred p] (hp : (setOf p).Finite) (n : ) :
      Nat.count p n hp.toFinset.card
      theorem Nat.count_lt_card {p : Prop} [DecidablePred p] {n : } (hp : (setOf p).Finite) (hpn : p n) :
      Nat.count p n < hp.toFinset.card
      theorem Nat.count_of_forall {p : Prop} [DecidablePred p] {n : } (hp : n' < n, p n') :
      Nat.count p n = n
      @[simp]
      theorem Nat.count_true (n : ) :
      Nat.count (fun (x : ) => True) n = n
      theorem Nat.count_of_forall_not {p : Prop} [DecidablePred p] {n : } (hp : n' < n, ¬p n') :
      Nat.count p n = 0
      @[simp]
      theorem Nat.count_false (n : ) :
      Nat.count (fun (x : ) => False) n = 0
      theorem Nat.count_mono_left {p : Prop} [DecidablePred p] {q : Prop} [DecidablePred q] {n : } (hpq : ∀ (k : ), p kq k) :