Complete S195 "Join of cofinite and left-ray topologies on ω1​"

[plp127]

I have many proofs to write down.
Currently trying to fill out the properties for S195

[prabau]

I have not read any of what you wrote. But a reminder: we don't want long, involved proofs in pi-base. Any such should be somewhere else, typically in mathse, and we can reference that. (longish but straightforward has been kind of accepted, but it's a judgment call).
@StevenClontz ?

[StevenClontz]

Agreed on both points: (1) I have not reviewed this, and (2) if there are many proofs to write out, they should be done elsewhere, so more people can see and review the mathematics.

[prabau]

@plp127 Reminder: if you want this to be reviewed, you can move this PR out of the draft state.

[prabau]

I don't think we can accept this PR.

As discussed previously, some of the proofs here are too involved for a direct proof in pi-base. As @StevenClontz has written in the References section of https://github.com/pi-base/data/wiki/Contributing:

pi-Base is not a forum for peer review, so
to contribute improvements not directly reflected in the literature, we encourage you to ask (and self-answer
if necessary) an appropriate question on either https://math.stackexchange.com/ or https://mathoverflow.net/,
and use that as your citation.

We sometimes make exceptions when the proof is really straightforward. But that is not the case in many of your justifications.

Also, it is much preferred to do several smaller PRs, which are easier to review, and provide a steady pace of incremental improvements. Absolutely nothing forces you to "complete" a space, except the title that you chose.
Mega PRs usually don't go anywhere in any reasonable amount of time, as there is usually too much to discuss and review.

---

I can write a few mathse questions for some of the more involved properties, and we can see what people answer with, including your solution if you want to add it there. And then we can refer to that in pi-base, after it has been vetted.

How does that sound? Other suggestions are fine too.

[plp127]

I was putting my proofs on this branch, so that I can use the pi-base web tools to figure out which properties are automatically deduced and which ones are left. Then I could reduce to a minimal spanning set and (????) getting reliable references and gradually add them to pi-base hopefully

I guess none of that requires having a draft PR open. I guess I'll close this then.

[prabau]

An explanation would have been helpful, but I don't think there was anything wrong with your plan.
It probably makes more sense to reopen the PR then, but keep this one as a placeholder in draft mode.
Can you add a note in the description at the top?

Note also that one can always create a separate branch for exploratory purposes even without an associated PR.

[prabau]

But again, one can always write small PRs with just a few traits and get that deployed as you go. Steady, incremental progress.

[prabau]

Final note: no need to worry about determining a minimal spanning set upfront. If some non-minimal traits are deployed first, they can be removed later on as other traits that can deduce them get added. We do this all the time.

[plp127]

Final note: no need to worry about determining a minimal spanning set upfront. If some non-minimal traits are deployed first, they can be removed later on as other traits that can deduce them get added. We do this all the time.

Because finding proofs is easy, and finding references is hard, I decided to use the plan that lets me not have to find as many references.