Theorems · Theorem · combinatorics
Finset.mem_range_succ_iff
∀ {a b : ℕ}, a ∈ Finset.range b.succ ↔ a ≤ b- Defined in
- Mathlib.Data.Finset.Range
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Finsetstatement · cited by 13,712
- Finset.rangestatement · cited by 1,341
Cited by22
Results whose statement or proof uses this declaration.
- Polynomial.bernoulli_defproof · cited by 4
- Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_evalproof · cited by 3
- HasFPowerSeriesAt.apply_eq_zeroproof · cited by 2
- Polynomial.Chebyshev.strictAntiOn_nodeproof · cited by 2
- Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iffproof · cited by 2
- bernoulli'_spec'proof · cited by 2
- PowerSeries.exp_mul_exp_eq_exp_addproof · cited by 2
- VectorFourier.norm_iteratedFDeriv_fourierPowSMulRightproof · cited by 2
- MeasureTheory.stronglyAdapted_predictablePartproof · cited by 2
- Polynomial.comp_C_mul_X_coeffproof · cited by 2
- Nat.smoothNumbersUpTo_card_add_roughNumbersUpTo_cardproof · cited by 1
- mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAtproof · cited by 1