Add "iff Kolmogorov ..." for most remaining properties

[felixpernegger]

Add "property holds iff for kolmogorov quotient" for almost all proerties where it is true. For weakly first countable for example, it could be true.

This is kind of a big PR, but most of the additions are trivial or at least easy (similar to #1674). I dont think it makes sense to artificially split this up.
Most of the addtions are originally by @danflapjax in his spreadsheet in #1198, which I expanded.

It's plausible there are some mistakes (sometimes taking the quotient can be confusing, i.e. for Sequential), so please check carefully.

(as you might can guess I used AI to get the data from the spreadsheet to the property files)

[prabau]

Are all these additions with "iff", or are there some implications in only one direction?

[felixpernegger]

Are all these additions with "iff", or are there some implications in only one direction?

All the ones I added to the spreadsheet are "iff", I cant speak for the old ones but I suspect the same.

[prabau]

If I remember correctly, the existing ones had some cases where only one implication was valid; don't remember which ones right now. There are also cases when the properties are not the same for $X$ and $Kol(X)$, for example pseudometrizable and metrizable.

[felixpernegger]

If I remember correctly, the existing ones had some cases where only one implication was valid; don't remember which ones right now. There are also cases when the properties are not the same for X and K o l ( X ) , for example pseudometrizable and metrizable.

I think you are right. I checked which of the properties changed imply T0 and it was only P46 (for which I removed the kolmogorov metaprop now). The rest is probably fine then.