Cleanup for S22 Fortissimo space on the reals #1207
Conversation
|
The build is failing, seemingly due to AWS problems. |
|
@yhx-12243 would you be able to review this? |
There was a problem hiding this comment.
No problems for now, if we don't care the unknown traits.
Among those unknown traits, P172 (Radial) is resolved in mathse:4833761, and all the others seems undecidable in ZFC.
Anyway, these can be postponed, depend on your intention.
|
Thanks for reviewing. My intention was to get this cleanup out of the way first. And then add more. Actually, like you said, many of the remaining traits are undecidable. I was thinking it would be useful to introduce two new spaces where these traits can be decided:
which are of course the same as S22 depending on some set-theoretic assumptions. That would provide a good way to illustrate why some of the traits are undecidable for S22. By I should probably open an issue first to see if this would be acceptable to add. Opinion? |
|
@yhx-12243 See #1213. |
Cleanup for S22 (Fortissimo space on the real numbers).
Removed redundant traits, and updated the README to something that seemed easier to grasp for me (and also more closely matches S154 (Fort space on the real numbers)).