Theorems · Theorem · order theory
Nat.Ico_zero_eq_range
∀ (a : ℕ), Finset.Ico 0 a = Finset.range a
- Defined in
- Mathlib.Order.Interval.Finset.Nat
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.rangestatement and proof · cited by 1,341
- Finset.Icostatement and proof · cited by 450
- Nat.bot_eq_zeroproof · cited by 8
- Nat.Iio_eq_rangeproof · cited by 6
- Finset.Iio_eq_Icoproof · cited by 3
Cited by25
Results whose statement or proof uses this declaration.
- Finset.range_eq_Icoproof · cited by 26
- Finset.sum_range_add_sum_Icoproof · cited by 12
- Finset.sum_Ico_eq_sum_rangeproof · cited by 10
- intervalIntegral.sum_integral_adjacent_intervalsproof · cited by 6
- eVariationOn.sum_le_of_monotoneOn_Iicproof · cited by 5
- AntitoneOn.sum_le_integral_Icoproof · cited by 3
- AntitoneOn.integral_le_sum_Icoproof · cited by 3
- Commute.add_pow_prime_pow_eq'proof · cited by 3
- AkraBazziRecurrence.asympBound_def'proof · cited by 3
- sub_one_mul_padicValNat_factorialproof · cited by 2
- dist_le_range_sum_distproof · cited by 2
- dist_le_range_sum_of_dist_leproof · cited by 2