Theorems · Theorem · number theory
Nat.findGreatest_le
∀ {P : ℕ → Prop} [inst : DecidablePred P] (n : ℕ), Nat.findGreatest P n ≤ n- Defined in
- Mathlib.Data.Nat.Find
- Cited by
- 7 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.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.findGreateststatement · cited by 25
- Nat.findGreatest_eq_iffproof · cited by 6
Cited by7
Results whose statement or proof uses this declaration.
- addRothNumber_leproof · cited by 3
- mulRothNumber_leproof · cited by 2
- Nat.findGreatest_mono_rightproof · cited by 2
- measurable_findGreatest'proof · cited by 1
- ruzsaSzemerediNumber_leproof · cited by 1
- PairReduction.iSup_edist_pairSetproof · cited by 1
- Set.finite_range_findGreatestproof · cited by 0