Theorems · Theorem · logic and foundations
Cardinal.cantor
∀ (a : Cardinal.{u}), a < 2 ^ aCantor's theorem
- Defined in
- Mathlib.SetTheory.Cardinal.Order
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Cardinalstatement and proof · cited by 2,598
- Function.Embeddingproof · cited by 988
- Cardinal.mkproof · cited by 942
- Cardinal.inductionOnproof · cited by 19
- Set.singleton_eq_singleton_iffproof · cited by 13
- Function.cantor_injectiveproof · cited by 3
- Cardinal.mk_setproof · cited by 3
- Function.Embedding.casesOnproof · cited by 3
Cited by12
Results whose statement or proof uses this declaration.
- Cardinal.aleph0_lt_continuumproof · cited by 11
- Cardinal.preBeth_strictMonoproof · cited by 9
- Cardinal.power_self_eqproof · cited by 6
- Cardinal.preBeth_limitproof · cited by 5
- Cardinal.mk_Ioi_realproof · cited by 3
- Cardinal.cantor'proof · cited by 2
- IsClosed.mk_lt_continuumproof · cited by 1
- Cardinal.IsStrongPrelimit.isSuccPrelimitproof · cited by 1
- ZFSet.card_vonNeumannproof · cited by 0
- not_countable_complexproof · cited by 0
- nonempty_embedding_to_cardinalproof · cited by 0
- IsClosed.mk_lt_two_pow_mk_denseproof · cited by 0