Add nonempty in definition of hyperconnected and ultraconnected #55
Conversation
There was a problem hiding this comment.
The change here generalizes the existing Theorem 110 by weakening the T4 hypothesis to normal with the same conclusion. As a result of this, three spaces that previously had "weakly countably compact" asserted will now have it deduced. This would allow to remove the corresponding property files for these spaces. What is the policy when a property for a space is both asserted and deduced?
The three spaces in question are:
- Right ordered reals (S42)
- Nested interval topology (S44)
- Divisor topology (S49)
|
@StevenClontz @jamesdabbs See the comment in PR #55 with this question from Aug 26. We now have some cases where a property for a given space is both asserted from an item in Steen & Seebach, and deduced from various theorems in the database. For example space S000042 (right ordered reals) is weakly countably compact, but this can now be deduced from T000110. In the generated data on the web site, assertions seem to take precedence over deductions. What is your preference about such cases? If we remove the files that assert these properties, that will convert it into a deduction and will slightly streamline the data in the database. If that is the recommended policy, let me know and I can do a pull request. |
|
There are pedagogical reasons to avoid the policy of strictly forbidding redundant assertions; even if a property can be deduced automatically, there might be a classic textbook reference for it as well. That said, if we implemented #16 we could simply omit the But if you've found a way to remove redundant assertions and they don't say anything beyond e.g. "Asserted in Counterexamples page XX" then I definitely don't mind removing them. Ideally this is something we should be able to do automatically down the road. I'll open an issue if we don't already have one to that effect. |
|
Makes sense about the pedagogical reasons. I'll take a closer look at a few cases. |
The empty set is disjoint from any other set. So to be strictly correct, the "nonempty" qualifier should be added in the definition of hyperconnected and ultraconnected spaces.