Theorems · Theorem · number theory
Nat.count_nth
∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ},
(∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → Nat.count p (Nat.nth p n) = n- Defined in
- Mathlib.Data.Nat.Nth
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidablePred
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- Set.ofPredstatement and proof · cited by 6,101
- Finset.cardstatement and proof · cited by 2,327
- Set.Finitestatement and proof · cited by 1,814
- Set.Finite.toFinsetstatement and proof · cited by 351
- Nat.nthstatement and proof · cited by 84
- Nat.countstatement and proof · cited by 55
- Finset.card_insert_of_notMemproof · cited by 45
- Nat.count_eq_card_filter_rangeproof · cited by 14
- Nat.filter_range_nth_eq_insertproof · cited by 3
- Nat.count_nth_zeroproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- Nat.nth_countproof · cited by 7
- Nat.count_nth_of_infiniteproof · cited by 3
- Nat.nth_lt_of_lt_countproof · cited by 2
- Nat.count_nth_of_lt_card_finiteproof · cited by 0
- Nat.count_nth_succproof · cited by 0