pi-base
Theorem Suggestion: no closed point => weakly countably compact
Theorem suggestions
- no closed point ~P107 $\Rightarrow$ weakly countably compact P21
- partition topology P185 + has closed point P21 $\Rightarrow$ has isolated point P139
We can look for other similar theorems in trivial cases.
Rationale
This theorem would demonstrate that no spaces satisfy the following search:
https://topology.pi-base.org/spaces?q=%7EHas+a+closed+point%2B%7EWeakly+countably+compact https://topology.pi-base.org/spaces?q=patrition+topology%2B%7EHas+isolated+point%2BHas+a+closed+point A few traits for partition topologies and other non- $T_0$ spaces may become redundant.
We may consider adding a space of the form "disjoint union of S194 and S2" to have a counterexample to https://topology.pi-base.org/spaces?q=%7ET0+%2B+%7EWeakly+countably+compact
Proofs
- Since $\overline{\{x\}}\setminus\{x\}\neq\emptyset$, every non-empty (in particular: infinite) set has an accumulation point.
- In partition topology every closed set is open, hence any closed point is isolated.
It would be ok to add these trivial results if it would make redundant some asserted traits of spaces.
Without that, I am not sure it's worth it. (We can always add it later when we have a use for them.)
Mostly the traits for simple (degenerate) spaces can be deduced in various ways and the initial assumptions could vary as well . I was originally inspired by the proof of P21 in #1439.
I see it for #1439 (S6). For this space, we may choose to assert P21 and derive P107 = false (which is how it is done now). Or assert P107 = false and derive P21.
We have to assert one of the two to make things work. And you are saying the justification for P107 = false would be easier (which I agree with). So that's a good reason to add this theorem. I would agree with that. Is that what you had in mind?
I was actually less precise, but yes. It would also make sense to search for other such examples. It is definitely of low priority.
It would be ok to add these trivial results if it would make redundant some asserted traits of spaces.
Without that, I am not sure it's worth it. (We can always add it later when we have a use for them.)
It definitely does make some of them redundant S5, S6 for example, probably more, especially the first theorem (not sure about the second one).
I definitely think the first theorem should be added, we can decide if the second is worth to add or not if you want.
