Theorems · Theorem · order theory
Int.card_uIcc
∀ (a b : ℤ), (Finset.uIcc a b).card = (b - a).natAbs + 1
- Defined in
- Mathlib.Data.Int.Interval
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.cardstatement · cited by 2,327
- absproof · cited by 1,814
- add_commproof · cited by 1,535
- Finset.card_mapproof · cited by 114
- Finset.card_rangeproof · cited by 108
- Finset.uIccstatement · cited by 84
- Function.Embedding.transproof · cited by 83
- add_sub_assocproof · cited by 72
- Nat.cast_injproof · cited by 70
- sub_nonneg_of_leproof · cited by 37
- addLeftEmbeddingproof · cited by 36
- Nat.castEmbeddingproof · cited by 29
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.