Theorems · Definition · logic and foundations
Set.encard
{α : Type u_1} → Set α → ℕ∞The cardinality of a set as a term in ℕ∞
- Defined in
- Mathlib.Data.Set.Card
- Cited by
- 327 results in Mathlib
- Foundations
- Depth 89 from the axioms, rests on 2,402 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by341
Results whose statement or proof uses this declaration.
- Set.ncardproof · cited by 344
- Matroid.eRankproof · cited by 36
- Set.Finite.cast_ncard_eqstatement and proof · cited by 28
- Set.encard_singletonstatement · cited by 26
- SimpleGraph.IsEdgeReachableproof · cited by 24
- Set.chainHeightproof · cited by 22
- Metric.coveringNumberproof · cited by 19
- SimpleGraph.vertexCoverNumproof · cited by 17
- Set.encard_emptystatement · cited by 17
- Set.encard_insert_of_notMemstatement and proof · cited by 17
- Set.encard_union_eqstatement and proof · cited by 15
- Set.encard_univstatement · cited by 15
Showing the 200 most cited of 341.