Theorems · Theorem · logic and foundations
ZFSet.card_powerset
∀ (x : ZFSet.{u}), x.powerset.card = 2 ^ x.card- Defined in
- Mathlib.SetTheory.ZFC.Cardinal
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetLike.coeproof · cited by 8,199
- Cardinalstatement · cited by 2,598
- Cardinal.mkproof · cited by 942
- ZFSetstatement and proof · cited by 259
- Cardinal.mk_congrproof · cited by 55
- Cardinal.lift_injproof · cited by 38
- ZFSet.cardstatement and proof · cited by 16
- ZFSet.powersetstatement · cited by 11
- Cardinal.lift_ofNatproof · cited by 7
- Cardinal.lift_powerproof · cited by 7
- Cardinal.mk_powersetproof · cited by 4
- ZFSet.powersetEquivproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- ZFSet.card_vonNeumannproof · cited by 0