Remove T2,4,5,6 => T1

[Jianing-Song]

Removed the implications $T_i\Rightarrow T_1$ for $i=2,4,5,6$ since they are not needed.

I also changed a bit the wording of T488.

[Jianing-Song]

Interestingly enough, note that we cannot remove "discrete => $T_1$" and "Fully $T_4$ => $T_1$", which are used respectively in "discrete => $T_6$" and "Fully $T_4$ => $T_4$".

[prabau]

T488: the fact that every sequence has a monotone subsequence has nothing to do with the topology. It is something that holds in any totally ordered set, which is why it's better to phrase the first sentence in terms of totally ordered set and not mention LOTS for that. The LOTS topology is used implicitly in the last sentence, so that a monotone sequence with an accumulation point converges to that value.

Note: If we did not mention it before, this illustrate why it's better not to mix multiple unrelated changes in the same PR. As the other changes in this PR also need discussion.

[prabau]

Some interesting thing to think about: Can T488 be generalized to GO-spaces: [countably compact + GO-space ==> sequentially compact] ?

For example in the Sorgenfrey line, which is a GO-space, an increasing sequence with a finite supremum does not converge. It has no accumulation point, and also no converging subsequence. So the space in neither countably compact, nor sequentially compact. Maybe there is some other counterexample, or maybe not.

[prabau]

As for the other changes, it is true that the removed theorems are not strictly necessary as they can be deduced. Whether it's a good idea or not can be debated though. The removed theorems can be viewed as "shortcut theorems" which help streamline some of the deductions. We have discussed this general issue a few times here in the past, without reaching a clear conclusion.

For example, see https://github.com/orgs/pi-base/discussions/319,
https://github.com/orgs/pi-base/discussions/528,
and pi-base/web#142.

I was worried in particular about T118 [T2 ==> T1]. There is a whole chain of implications from T2 to T1 via KC, US, and various intermediate properties. But comparing π-Base, Search for T2+~T1 with and without the change shows there is an alternate route with just one extra step, thanks the intermediate Locally Hausdorff property. So not that bad.

On the other hand, for example from T5 to T1 used to be one step and would now be seven steps: π-Base, Search for T5+~T1. And that gets compounded if used as a subproof in a more complicated deduction. But is that significant? Maybe not.

I think this change would benefit from the input of more than two people. Pinging @marswill and @danflapjax in addition to @ccaruvana and @StevenClontz.

[Jianing-Song]

T488: the fact that every sequence has a monotone subsequence has nothing to do with the topology. It is something that holds in any totally ordered set, which is why it's better to phrase the first sentence in terms of totally ordered set and not mention LOTS for that. The LOTS topology is used implicitly in the last sentence, so that a monotone sequence with an accumulation point converges to that value.

Note: If we did not mention it before, this illustrate why it's better not to mix multiple unrelated changes in the same PR. As the other changes in this PR also need discussion.

Yes, I realized that now it's difficult to handle this PR with the changes. I am really sorry for the inconvenience caused!

I will make a separated PR for the minor changes not involving deleting files.

I see you points about deleting the implications of $T_1$. If the final decision is that we should delete them, I will make another PR to do that. Now let's leave this PR just for discussion.

[StevenClontz]

What I'd really like is a way (i.e. an update to pi-Base software) to keep theorems like $T_2\Rightarrow T_1$ but instead of providing a written proof, we can just point out that it's a consequnce of other theorems in $\pi$-Base. Then when we have $P\Rightarrow R$ as a theorem, and we introduce $Q$ with the theorems $P\Rightarrow Q$ and $Q\Rightarrow R$, we don't need to delete $P\Rightarrow R$, but instead point to those two new theorems.

[prabau]

What I'd really like is a way (i.e. an update to pi-Base software) to keep theorems like T2⇒T1 but instead of providing a written proof, we can just point out that it's a consequnce of other theorems in π-Base. Then when we have P⇒R as a theorem, and we introduce Q with the theorems P⇒Q and Q⇒R, we don't need to delete P⇒R, but instead point to those two new theorems.

Maybe you mean that we do delete P=>R, but it's still available. I don't think we want to have a cluttered database with many redundant theorems that can be deduced from other ones. But @danflapjax and @marswill 's suggestions were to somehow keep internally a record of what can be deduced and then somehow apply that as needed, without the need to keep the redundant theorems explicitly.

[StevenClontz]

We discussed in today's call and agreed that this was correctly closed. Thanks @Jianing-Song!