Theorems · Theorem · number theory
Nat.find_mono
∀ {p q : ℕ → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q],
(∀ (n : ℕ), q n → p n) → ∀ {hp : ∃ n, p n} {hq : ∃ n, q n}, Nat.find hp ≤ Nat.find hqA weak version of Nat.find_mono_of_le, requiring q implies p everywhere.
- Defined in
- Mathlib.Data.Nat.Find
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses no axioms
- Assumes
- DecidablePredDecidablePred
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.findstatement and proof · cited by 139
- Nat.find_mono_of_leproof · cited by 2
Cited by10
Results whose statement or proof uses this declaration.
- Subgroup.lowerCentralSeries_length_eq_nilpotencyClassproof · cited by 5
- AddSubgroup.lowerCentralSeries_length_eq_nilpotencyClassproof · cited by 4
- Group.nilpotencyClass_le_of_surjectiveproof · cited by 2
- Subgroup.least_ascending_central_series_length_eq_nilpotencyClassproof · cited by 2
- Subgroup.least_descending_central_series_length_eq_nilpotencyClassproof · cited by 2
- AddGroup.nilpotencyClass_le_of_surjectiveproof · cited by 1
- AddSubgroup.least_ascending_central_series_length_eq_nilpotencyClassproof · cited by 1
- AddSubgroup.least_descending_central_series_length_eq_nilpotencyClassproof · cited by 1
- Subgroup.nilpotencyClass_leproof · cited by 0
- AddSubgroup.nilpotencyClass_leproof · cited by 0