Open Almanzoris opened 4 days ago
Depending on what everyone decides to do with Issue https://github.com/pi-base/data/issues/940, a theorem involving that property (currently number 3 on the list) could be referenced. Edit: Or maybe this one gets deduced automatically?
Good point! I hadn't read this... I could close it or change it to Homogeneous + Has a closed point ==> $T_1$, which would be the number 6 in the list. But, I wouldn't mind closing it, knowing that you have opened the issue before me making the PR. You probably have proven it already.
Maybe don't close it until that issue gets resolved. If you have the time, maybe you could weigh in any thoughts you have on that issue?
Alright! I will read it better later today. I already agree with adding the property "Has a closed point".
I already agree with adding the property "Has a closed point".
Oh sorry I didn't notice you did!
This will indeed get automatically deduced if has a closed point and the theorems referenced in #940 is added. Indeed, combining theorems 3 and 6 in #940, and https://topology.pi-base.org/spaces?q=Homogeneous+%2B+Has+a+cut+point+%2B+Has+an+isolated+point gives the result.
Yeah, I just missed the issue.
T209 could be referenced.
I'm going to reword the second either ... or ...; if the cut point is open, it would be reached that it is closed aswell.