Abstract
We present a new succinct proof of the uncountability of the real numbers – optimized
for clarity – based on the proof by Benjamin Porter in the Isabelle Analysis theory.
for clarity – based on the proof by Benjamin Porter in the Isabelle Analysis theory.
| Original language | English |
|---|---|
| Publication date | 2018 |
| Number of pages | 6 |
| Publication status | Published - 2018 |
| Event | International Workshop on Theorem proving components for Educational software - Oxford , United Kingdom Duration: 18 Jul 2018 → 18 Jul 2018 http://www.uc.pt/en/congressos/thedu/thedu18/programme |
Conference
| Conference | International Workshop on Theorem proving components for Educational software |
|---|---|
| Country/Territory | United Kingdom |
| City | Oxford |
| Period | 18/07/2018 → 18/07/2018 |
| Internet address |