pi-base
Add some traits for S18 Double pointed cocountable topology on R
One things noticeable is that, we can check all the theorems and strengthen it to the version that could be pass Kolmogorov quotient, that will be good for spaces like S18 whose Kolmogorov quotient has more property can be deduced.
For example, clearly $T_1$ in T381 can be weaken to $R_0$ and thus we would know {S18|¬P158}, etc.
Maybe it can be proposed in a separated issue/PR. Maybe a huge work.
P71 (sigma-relatively compact): This seems to relies of some meta-property involving the Kolmogorov quotient. If we are going to rely on that, that meta-property should be added to P71 (and carefully examine what the meta-property is actually).
I would love this PR to be finished for the sake of establishing which properties are known with more ease.
@StevenClontz Can you add the meta-properties as mentioned above? If you cannot do it, let me know and I'll add a commit for it in this PR.
@prabau I'm fine if you want to add them; I'm at a conference the next few days and wouldn't get to this until later in the week at the soonest.
I have added a commit for the meta-properties. But the changes don't show up in preview mode in the web interface.
@StevenClontz Does this have to do with the "Upload bundle to R2" step in compile.yml, that was restored in the main branch, but not in the current branch? If so, one needs to do a merge of the main branch into this branch. Not sure how to do this myself. So I'll let Steven handle it next week.
@Moniker1998 Thanks for reviewing. I'll merge it and hopefully everything will be fine.
Result: everything ok.