Theorems · Definition · logic and foundations
ZFSet.card
ZFSet.{u} → Cardinal.{u}The cardinality of a ZFC set.
- Defined in
- Mathlib.SetTheory.ZFC.Cardinal
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 25 from the axioms · 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.
- Cardinalstatement · cited by 2,598
- Cardinal.mkproof · cited by 942
- ZFSetstatement and proof · cited by 259
- Shrinkproof · cited by 132
Cited by16
Results whose statement or proof uses this declaration.
- ZFSet.cardinalMk_coe_sortstatement · cited by 7
- ZFSet.card_emptystatement · cited by 2
- ZFSet.card_insertstatement and proof · cited by 2
- Ordinal.card_le_card_vonNeumannstatement and proof · cited by 1
- ZFSet.iSup_card_le_card_iUnionstatement and proof · cited by 1
- Ordinal.card_toZFSetstatement · cited by 1
- ZFSet.card_monostatement · cited by 1
- ZFSet.card_powersetstatement and proof · cited by 1
- ZFSet.card_singletonstatement and proof · cited by 1
- ZFSet.lift_card_iUnion_le_sum_cardstatement and proof · cited by 1
- ZFSet.card_image_lestatement · cited by 0
- ZFSet.card_insert_lestatement and proof · cited by 0