Timeline for Uncountability of the real numbers from LLPO without countable choice
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 20, 2022 at 19:29 | comment | added | James E Hanson | I see. Thank you. | |
| Feb 20, 2022 at 19:17 | comment | added | Andrej Bauer | @JamesHanson: if you are referring to the construction of $s$ from $a$, then note that I never claimed it to be equality preserving. In fact it is not, nor does it need to be for the purposes of proving the theorem (which only requires existence of $s$). I hope I was careful enough to distinguish operations from functions (equality preserving operations). | |
| Feb 20, 2022 at 17:06 | comment | added | James E Hanson | Is it obvious that the function constructed in the theorem respects the imposed notion of equality (i.e., if I input different sequences of Cauchy sequences representing the same sequence of reals, I get the same real out)? | |
| Mar 21, 2020 at 16:12 | comment | added | Andrej Bauer | Absolutely, thanks and fixed. | |
| Mar 21, 2020 at 16:12 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
edited body
|
| Mar 21, 2020 at 10:35 | comment | added | David Roberts♦ | Surely Bishop would require $1/m+1/n$, not $1/m - 1/n$? | |
| Mar 21, 2020 at 10:20 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 16 characters in body
|
| Mar 21, 2020 at 10:13 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 3 characters in body
|
| Mar 21, 2020 at 8:24 | history | answered | Andrej Bauer | CC BY-SA 4.0 |