Counting on ℕ

This file provides lemmas about the relation of Nat.count with cardinality functions.

theorem Nat.count_le_cardinal {p : ℕ → Prop} [DecidablePred p] (n : ℕ) : ↑(count p n) ≤ Cardinal.mk ↑{k : ℕ | p k}

theorem Nat.count_le_setENCard {p : ℕ → Prop} [DecidablePred p] (n : ℕ) : ↑(count p n) ≤ {k : ℕ | p k}.encard

theorem Nat.count_le_setNCard {p : ℕ → Prop} [DecidablePred p] (n : ℕ) (h : {k : ℕ | p k}.Finite) : count p n ≤ {k : ℕ | p k}.ncard