Theorems · Theorem · logic and foundations
ZFSet.cardinalMk_coe_sort
∀ {x : ZFSet.{u}}, Cardinal.mk ↥x = Cardinal.lift.{u + 1, u} x.cardZFSet.card x is equal to the cardinality of x as a set of ZFSets.
- Defined in
- Mathlib.SetTheory.ZFC.Cardinal
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 27 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.
- Cardinalstatement and proof · cited by 2,598
- Cardinal.mkstatement and proof · cited by 942
- Cardinal.liftstatement and proof · cited by 583
- ZFSetstatement and proof · cited by 259
- ZFSet.cardstatement · cited by 16
- Cardinal.lift_mk_shrink''proof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- ZFSet.card_emptyproof · cited by 2
- Ordinal.card_toZFSetproof · cited by 1
- ZFSet.card_monoproof · cited by 1
- ZFSet.iSup_card_le_card_iUnionproof · cited by 1
- ZFSet.lift_card_iUnion_le_sum_cardproof · cited by 1
- ZFSet.card_image_leproof · cited by 0
- ZFSet.lift_card_range_leproof · cited by 0