Count

📁 Source: Mathlib/Data/Nat/Count.lean

Statistics

Metric	Count
Definitions `fintype`, `count`	2
Theorems `count_add`, `count_add'`, `count_eq_card_filter_range`, `count_eq_card_fintype`, `count_false`, `count_iff_forall`, `count_iff_forall_not`, `count_injective`, `count_le`, `count_le_card`, `count_lt_card`, `count_lt_count_succ_iff`, `count_mono_left`, `count_monotone`, `count_ne_iff_exists`, `count_of_forall`, `count_of_forall_not`, `count_one`, `count_strict_mono`, `count_succ`, `count_succ'`, `count_succ_eq_count`, `count_succ_eq_count_iff`, `count_succ_eq_succ_count`, `count_succ_eq_succ_count_iff`, `count_true`, `count_zero`, `exists_of_count_lt_count`, `lt_of_count_lt_count`	29
Total	31

Nat

Definitions

Name	Category	Theorems
`count` 📖	CompOp	48 math math: `count_add'`, `count_false`, `count_eq_card_filter_range`, `count_mono_left`, `count_le_setENCard`, `count_true`, `le_nth_count`, `count_le_cardinal`, `count_eq_card_fintype`, `count_nth_of_lt_card_finite`, `count_le_iff_le_nth`, `count_nth_succ_of_infinite`, `count_succ`, `count_succ_eq_count`, `count_zero`, `gc_count_nth`, `surjective_count_of_infinite_setOf`, `count_succ_eq_count_iff`, `count_monotone`, `count_modEq_card`, `count_add`, `count_le_card`, `count_le_setNCard`, `count_succ'`, `count_of_forall`, `count_nth`, `le_nth_count'`, `count_nth_of_infinite`, `count_one`, `count_strict_mono`, `count_lt_count_succ_iff`, `count_lt_card`, `count_nth_succ`, `count_succ_eq_succ_count`, `le_nth_of_count_le`, `nth_count`, `lt_nth_iff_count_lt`, `count_modEq_card_eq_ceil`, `count_succ_eq_succ_count_iff`, `count_le`, `count_iff_forall_not`, `count_of_forall_not`, `count_eq_zero`, `filter_multiset_Ico_card_eq_of_periodic`, `nth_count_eq_sInf`, `count_iff_forall`, `count_nth_zero`, `filter_Ico_card_eq_of_periodic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_add` 📖	mathematical	—	`count`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `count_eq_card_filter_range` `Finset.filter.congr_simp` `Finset.range_add` `Finset.filter_union` `Finset.card_union_of_disjoint` `Finset.filter_map` `add_right_injective` `Finset.card_map`
`count_add'` 📖	mathematical	—	`count`	—	`add_comm` `count_add` `count.congr_simp`
`count_eq_card_filter_range` 📖	mathematical	—	`count` `Finset.card` `Finset.filter` `Finset.range`	—	`count.eq_1`
`count_eq_card_fintype` 📖	mathematical	—	`count` `Fintype.card` `CountSet.fintype`	—	`count_eq_card_filter_range` `Fintype.card_of_subtype`
`count_false` 📖	mathematical	—	`count`	—	`count_of_forall_not`
`count_iff_forall` 📖	mathematical	—	`count`	—	`count_eq_card_filter_range` `Finset.card_range` `Finset.card_filter_eq_iff`
`count_iff_forall_not` 📖	mathematical	—	`count`	—	`count_eq_card_filter_range`
`count_injective` 📖	—	`count`	—	—	`count_strict_mono`
`count_le` 📖	mathematical	—	`count`	—	`count_eq_card_filter_range` `LE.le.trans_eq` `Finset.card_filter_le` `Finset.card_range`
`count_le_card` 📖	mathematical	—	`count` `Finset.card` `Set.Finite.toFinset` `setOf`	—	`count_eq_card_filter_range` `Finset.card_mono` `Set.Finite.mem_toFinset` `Finset.mem_filter`
`count_lt_card` 📖	mathematical	—	`count` `Finset.card` `Set.Finite.toFinset` `setOf`	—	`LT.lt.trans_le` `count_lt_count_succ_iff` `count_le_card`
`count_lt_count_succ_iff` 📖	mathematical	—	`count`	—	—
`count_mono_left` 📖	mathematical	—	`count`	—	—
`count_monotone` 📖	mathematical	—	`Monotone` `instPreorder` `count`	—	`monotone_nat_of_le_succ`
`count_ne_iff_exists` 📖	—	—	—	—	—
`count_of_forall` 📖	mathematical	—	`count`	—	`count_iff_forall`
`count_of_forall_not` 📖	mathematical	—	`count`	—	`count_iff_forall_not`
`count_one` 📖	mathematical	—	`count`	—	`count_succ` `count_zero` `zero_add`
`count_strict_mono` 📖	mathematical	—	`count`	—	`LT.lt.trans_le` `count_lt_count_succ_iff` `count_monotone`
`count_succ` 📖	mathematical	—	`count`	—	—
`count_succ'` 📖	mathematical	—	`count`	—	`count_add'` `count_one`
`count_succ_eq_count` 📖	mathematical	—	`count`	—	`count_succ_eq_count_iff`
`count_succ_eq_count_iff` 📖	mathematical	—	`count`	—	—
`count_succ_eq_succ_count` 📖	mathematical	—	`count`	—	`count_succ_eq_succ_count_iff`
`count_succ_eq_succ_count_iff` 📖	mathematical	—	`count`	—	—
`count_true` 📖	mathematical	—	`count`	—	`count_of_forall`
`count_zero` 📖	mathematical	—	`count`	—	—
`exists_of_count_lt_count` 📖	mathematical	`count`	`Set` `Set.instMembership` `Set.Ico` `instPreorder`	—	`lt_of_count_lt_count` `count_ne_iff_exists` `LT.lt.ne'` `count_add` `add_assoc`
`lt_of_count_lt_count` 📖	—	`count`	—	—	`Monotone.reflect_lt` `count_monotone`

Nat.CountSet

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	1 math math: `Nat.count_eq_card_fintype`

---

← Back to Index