Theorems · Definition · logic and foundations
Set.ncard
{α : Type u_1} → Set α → ℕThe cardinality of s : Set α . Has the junk value 0 if s is infinite
- Defined in
- Mathlib.Data.Set.Card
- Cited by
- 344 results in Mathlib
- Foundations
- Depth 90 from the axioms, rests on 2,405 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.encardproof · cited by 327
- ENat.toNatproof · cited by 143
Cited by352
Results whose statement or proof uses this declaration.
- Set.Finite.cast_ncard_eqstatement · cited by 28
- Set.ncard_eq_toFinset_cardstatement · cited by 21
- Set.ncard_univstatement · cited by 21
- ProbabilityTheory.binomialproof · cited by 20
- Nat.card_coe_set_eqstatement · cited by 19
- Set.ncard_add_ncard_complstatement and proof · cited by 16
- Set.ncard_le_ncardstatement and proof · cited by 15
- Set.ncard_coe_finsetstatement · cited by 15
- Set.ncard_emptystatement · cited by 14
- Set.fintypeCard_eq_ncardstatement · cited by 13
- SimpleGraph.IsCyclesproof · cited by 12
- Set.Infinite.ncardstatement · cited by 12
Showing the 200 most cited of 352.