Commit 2021-12-17 12:31 8743573e

View on Github →

feat(data/nat/count): The count function on naturals (#9457) Defines nat.count a generic counting function on ℕ, computing how many numbers under k satisfy a given predicate". Co-authored by: Yaël Dillies, [email protected] Vladimir Goryachev, [email protected] Kyle Miller, [email protected] Scott Morrison, [email protected] Eric Rodriguez, [email protected]

Estimated changes

Created src/data/nat/count.lean

added def nat.count

added theorem nat.count_add'

added theorem nat.count_add

added theorem nat.count_eq_card_filter_range

added theorem nat.count_eq_card_fintype

added theorem nat.count_le_cardinal

added theorem nat.count_mono_left

added theorem nat.count_monotone

added theorem nat.count_one

added def nat.count_set.fintype

added theorem nat.count_succ'

added theorem nat.count_succ

added theorem nat.count_succ_eq_count_iff

added theorem nat.count_succ_eq_succ_count_iff

added theorem nat.count_zero

added theorem nat.lt_of_count_lt_count