feat: T_D property and theorems

[artemetra]

The $T_D$ property from #1836.
This PR adds the property, some theorems and traits.

Let me know if there are any comments. As is, there are only 5 spaces that cannot deduce $T_D$ automatically, so perhaps those need to be filled out manually, but this PR is getting a bit long so I'd rather merge before continuing with those.

[prabau]

S82-P247: the way this is phrased makes it seem that you are using a meta-property related to direct sums. But in fact we need to use hereditariness. So please rephrase (for example "X contains a subspace homeomorphic to ... and ..." .)

[prabau]

For the definition, I don't think the characterization that the derived set of every subset is closed should be the main one.
We can and should list it in the list of equivalent ones (and need to mention some specific ref for it, as it's not obvious: Theorem 5.1 in Aull & Thron covers it for example).

For the main definition, I am still debating what the most convenient one would be, for use in proving traits in particular. Both Aull & Thron and Encyclopedia of general topology (Hart, Nagata, Vaughan) use $\overline{\{x\}}\setminus\{x\}$ is closed for every $x\in X$ (i.e., the derived set of singletons is closed). Of course it's equivalent to the other ones you have. I also think we need to look at more sources, not just Picado/Pultr, to see what is commonly used.

Feel free to modify things and then we can look more.

[prabau]

Looking at S42-P147, we need to show that the space is not T_D. Seems to me using the definition in terms of derived sets of singletons is more convenient. One just computes:
$\overline{\{x\}}\setminus\{x\}=(\leftarrow,x]\setminus\{x\}=(\leftarrow,x)$, which is not closed since $x$ is an accumulation point of $(\leftarrow,x)$.
That would be more straightforward (less "busy") than what is there right now in terms of open sets $U$.

That seems to be an indication that it would be a good primary definition. It seems that the proof of several of the theorems here can also be simplified with that approach.

What do you think?

[prabau]

the pi-base guidelines prefer to use zb