Traits for S140: \mathbb{R} extended by a point with cocountable open neighborhoods#1656
Traits for S140: \mathbb{R} extended by a point with cocountable open neighborhoods#1656mathmaster13 wants to merge 12 commits intomainfrom
Conversation
Yes. |
Any advice for writing SE questions? I feel like "Is |
"Does |
this is fine |
|
Yeah, being too terse may get the question closed (= rejected). Give a description of the space, explain why this space is interesting. Then ask about the alpha_i properties in general. Need to give a precise description of what you mean by these properties. (Usually, if the post is not reasonably self contained, it may also get closed. Maybe it's enough to refer to some other post for details in this case?) Tell what is already known for the space, related to the alpha_i properties. Basically, need to make the question interesting. Also, you can either ask and answer yourself. Or better, have someone else write the question and then you answer later. |
If you want this done quickly, if someone who actually knows about the alpha i properties/their motivation (I know nothing about them beyond the proof I just did, so I'd have to learn that), then they should write it. I likely will be slower to contribute this weekend. |
|
just copy from https://math.stackexchange.com/questions/5123855 for example |
|
I wrote this. Not sure if it's good. Feel free to give suggestions. I saw y'all shamelessly copy the intro from each other so I did too. |
|
Looks good to me, maybe consider linking https://topology.pi-base.org/spaces/S000140 when you introduce the space. Now best just post your own answer (since you have it already) to the question, no need to overcomplicated this |
|
Btw, I think its a good idea to rename S140 to "$\mathbb{R}$ extended by a point with cocountable open neighborhoods$ in this PR and explicitly linking S25 in the description. |
Link S25 in S140's pibase description? |
Similar as its done in S50 maybe |
done |
|
P73's on the border and may also need to be SE'd. Let me know |
|
@mathmaster13 Nicely written mathse question. (I still need to read the answer.) |
Done. Thanks |
|
For the answer it's not clear what it's trying to do. A bird's eye view should be able to tell if you are trying to show it is or is not alpha_1, without having to dig into the details. Can you add a clear summary at the top? |
Thanks for the feedback. Let me know how I did. |
|
Much better! The subheadings are too big though, like shouting :-) You could for example replace the |
Haha, I don't catch these things because I write everything on a phone. So thanks! Did it. |
|
P73 might need to be a mathse question? It's kind of a boring/simple question but also kind of long. |
|
I'll review this PR later today. |
|
As suggested in #1656 (comment), it would also be good to replace |
|
Just wondering, did you check if adding the new traits makes any of the previous traits redundant? Don't worry if not. pi-base/web#232 would be really handy here. |
Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Sure, I guess. Is this consistent with other spaces? I feel like I've seen both kinds of names here. But sure, why not. I'll do it. I didn't check if it makes traits redundant, as far as I'm aware. |
Years ago all the names were basically in English words. Then, with changes to accept LaTeX in names, we started introducing more symbols where it made sense. In particular, in this case the name was quite unwieldy and I agree that using mathbb R makes things easier to grasp. But there are no hard and fast rules. Every case should be discussed separately if necessary. |
|
P73: A style thing. No need to have Seems ok to have the proof directly in pi-base, as it's not too complicated. But I want to look in more detail. Will continue tomorrow. |
P210 may be more suitable for stack exchange; let me know.
As a bonus, this PR provides another justification for why S140 is connected through the proof of sigma-connectedness. The automatic deduction pi-base displays, which uses "strongly connected" is circular because the proof of strong connectedness relies on the assumption of connectedness. That being said, strong connectedness is still what displays as the proof, so I can just put a note in to see the proof for sigma-connectedness, if that is worthwhile.
Note that there is already a proof of X's connectedness as a corollary of our proof that X is locally connected. But it isn't linked to either, so you just see strong connectedness and assuming X is connected with no reference.