Library ▹ Essentials ▹ Numbers ▹ Cardinal numbers
Theorem 1.8.2.22 (Cantor's theorem).  Let S be a set. Then:
|P(S)| > |S|
No proof.
References.
  • https://en.wikipedia.org/wiki/Cantor%27s_theorem
  • https://mathworld.wolfram.com/CantorsTheorem.html
  • https://proofwiki.org/wiki/Cantor%27s_Theorem
  • https://ncatlab.org/nlab/show/Cantor%27s+theorem
  • http://us.metamath.org/mpegif/canth2.html
  • https://leanprover-community.github.io/mathlib_docs/set_theory/cardinal.html#cardinal.cantor
[View Source]