Closed prabau closed 4 months ago
Out of curiosity: Why is the new property numbered as P154? It seems to me that there are many gaps among the labels of the properties, so why didn't we use P83 (the smallest gap)?
Out of curiosity: Why is the new property numbered as P154? It seems to me that there are many gaps among the labels of the properties, so why didn't we use P83 (the smallest gap)?
I wanted a number larger that P133 (LOTS). But not a compelling reason, really.
Out of curiosity: Why is the new property numbered as P154? It seems to me that there are many gaps among the labels of the properties, so why didn't we use P83 (the smallest gap)?
I wanted a number larger that P133 (LOTS). But not a compelling reason, really.
Ah yes, that makes sense. Thanks!
Adding GO-space as a new property, together with related theorems.
Some of the remaining theorems for LOTS can possibly also be converted to GO-spaces, but it's a first batch. I'll do a later PR to add the property for spaces like the Sorgenfrey line or the Michael line.