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 |