Theorems · Theorem · number theory
Nat.count_strict_mono
∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → m < n → Nat.count p m < Nat.count p n- Defined in
- Mathlib.Data.Nat.Count
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 67 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LT.lt.trans_leproof · cited by 678
- Nat.countstatement · cited by 55
- Nat.count_monotoneproof · cited by 4
- Nat.count_lt_count_succ_iffproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- Nat.nth_count_eq_sInfproof · cited by 1
- Nat.count_injectiveproof · cited by 1