List of theorems generalized by Kolmogorov quotient

[felixpernegger]

There has been talk of automising this task. I personally find this really not so important.

However, I made a list of many theorems that can be generalised with the kolmogorov quotient (and are not yet captured by the deduction engine)

This is probably not comprehensive, but shouldnt be too far away from all theorems that can be generalised. I used the spreadsheet (which I expanded slightly) in #1198 by @danflapjax and I small script (by Claude Code) to find these theorems. One should double check the results are true.
Also note "Noetherian + Artinian" is equivalent to "Finitely many open sets" (which I think should be its own property...), which can yet yet be deduced but could be if #1465 were merged.

[prabau]

This was already discussed several times in the past. Just because a theorem can be generalized in this fashion does not mean we necessarily need to change it or add a non-T0 version for it.

Ideally, the deduction engine would be enhanced to understand Kolmogorov quotients and we would not even need to do all of this, and would be able to concentrate on T0 versions of the theorems for most of them.

[prabau]

@StevenClontz FYI

[felixpernegger]

@prabau what is the main arguement behind not manually adding non-t0 generalisations? In my opinion this is just a strict imrpovement (to the deduction engine)

[prabau]

One of the principles of pi-base has always been, and continues to be in my opinion, to foster human understanding (more than automatically deducing theorems).

If we introduce non-T0 versions of existing theorems, there are two ways to go about it. Either we keep the old theorem and add a parallel version without T0, but that clutters things and makes it more difficult for a human to grasp all the theorems related to a property for example. Or we replace the old theorem by a new version, but that very often obscures things. In the sense that often the old theorem is well-known and easier to grasp, but the new version is sometimes more messy to prove and is not always obviously recognizable as the same thing and we lose visibility of the well-known result.

These things can be debated. But in my opinion, if adding non-t0 versions does not even help derive new traits, it is not worth it most of the time. The ideal solution will be to enhance the deduction engine to understand Kolmogorov quotients automatically.

@StevenClontz FYI

[StevenClontz]

Agreed @prabau