pi-base
Complete S195 "Join of cofinite and left-ray topologies on ω1"
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 ?
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.
@plp127 Reminder: if you want this to be reviewed, you can move this PR out of the draft state.
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.
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.
But again, one can always write small PRs with just a few traits and get that deployed as you go. Steady, incremental progress.
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.
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.