Define a typeclass for GO-space

[CoolRmal]

The definition of a GO-space can be found here: https://topology.pi-base.org/properties/P000154

Also prove the following lemmas:

1. A linearly ordered space is a GO-space.
2. A separable GO-space is hereditarily separable.
3. Optional: other lemmas that you can find on https://topology.pi-base.org/properties/P000154.

This is mentioned in #41918.

[nickcollins]

I'm working on this issue -- if I'm not able to complete it soon, I will plan to release it (by editing this comment) so that others will know it's uncontended again. Seems like an interesting problem!

[ParJai]

I'm working on this issue -- if I'm not able to complete it soon, I will plan to release it (by editing this comment) so that others will know it's uncontended again. Seems like an interesting problem!

Hi @nickcollins! I'd actually started working on this a few days ago, but I completely forgot to comment, my mistake. Since you're just getting going too, would you be open to splitting it? I could take one of the lemmas, or we could just compare notes? Happy to let you do it solo as well if you'd like, that's fully my fault for not commenting earlier. Let me know what works!

[nickcollins]

Hi @nickcollins! I'd actually started working on this a few days ago ...

Hey ParJai, no big -- if you already have the typeclass definition worked out, and have settled on which of the equivalent definitions to go with (I was actually thinking of switching to "homeomorphic to a subspace of a LOTS" because that might make it easier to prove the second lemma), why don't you go ahead and develop what you have, and post a draft or something, and then I can just work on some lemmas? I could take one of the lemmas mentioned in the original post, or if you're already partway through both of them, I could work on proving equivalence with one or more of the alternative definitions (which may be useful to anyone who depends on this but is working with one of the alternate characterizations), or work on some of the other theorems/lemmas mentioned in the pi-base link (just to flesh out the module a bit more)

[nickcollins]

Oh btw @ParJai , if I misunderstood and you haven't already put together the typeclass def yet, I could go ahead and do that, and do one of the lemmas, and leave you with the other one. Up to you.

[ParJai]

Oh btw @ParJai , if I misunderstood and you haven't already put together the typeclass def yet, I could go ahead and do that, and do one of the lemmas, and leave you with the other one. Up to you.

Sure, I didn't make too much progress yet. Feel free to take the typeclass def and a lemma, I can take up the other and some of the other things you mentioned, like proving equivalence with the alternative definitions.