Repository navigation
Locally orderable (part 4) - #1416
Conversation
|
The removal of redundant P120 for S86 and S209 was already merged into If you merge |
|
Is there a different way than a reverse direction PR? |
|
It all depends on what system you use to edit the PR. But definitely no need to have another PR. One commit within the same PR should be enough. If you use the command line, you can use Maybe doing nothing will be fine too, as the merge will just ignore it. |
The change of two PR of this part are same (compatible) so we needn't take care of this duplicate removal, just forward. (Or you can |
|
S59-P82: I am a little confused by the argument. What does "rational numbers in Also, to make sure I understand the previous part: To show the Euclidean closure of Minor: typo "cathegory" -> "category" |
|
Rational numbers should be dense but they have positive distance |
|
Hmm. Ok for the meaning. But still confused. The rational numbers are NOT dense in |
Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
|
S71-P120: (Irregular lattice topology is locally orderable) Given the order defined on (1) For points in (2) A typical nbhd of the origin point |
|
I'm not convinced. Also do not see a mistake in the current version. |
|
S71: Thanks for the update. But I don't think the equation in item (2): |
|
Points |
|
Ah, yes. Now I see it. I somehow had confused the order of the coordinates in my mind. |
|
S185-P120 (one-point compactification of the metric fan is locally orderable): Some ideas: There is a homeomorphism of For that, use a bijection from |
Good to know. @pzjp Should we remove the proposed change for S185 for now? Then add something after this proposed T462 change is done. |
|
T462 wouldn't help for S185. So we can just reference the result of S202 (although if these PR merged first, it will get a bad reference to somewhat “S202 ? P133”). |
|
The only other thing for me in this PR is Given a element I may actually be off by one for the |
I know T462 will not help for S185. What I am suggesting is to not do anything for S185 right now. And then do it after (or at the same time also ok) as T462. |
|
P120 for S185 would be resolved by the "local version of T462". See #1413. Although I do not know when and in what form it will be added. Unlike the global result, this does not seem natural to split. |
Actually |
P120 decided for few more spaces.
For all other spaces I know the answer seem to become derivable in the future (see #1413, #1388).
Removed locally 1-Euclidean ones.
Some minor cleanup.