Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Cardinality of the Continuum

Email Gateway (Nov 26 2023 at 10:24):

From: Dmitriy Traytel <traytel@di.ku.dk>
A concise, elegant AFP entry that Georg Cantor would be proud of, by Manuel Eberl. The abstract contains too much math to be shown faithfully here. TL;DR: the set of real numbers has the same cardinality as the powerset of natural numbers.

https://www.isa-afp.org/entries/Cardinality_Continuum.html

Enjoy!

Last updated: Jan 04 2025 at 20:18 UTC