[Feature wish] metric space is T4

[t6s]

It would be nice to have many exercise-level facts proved in the library, which would support the consistency of our formalization. An example is that every metric space is T4 (or "normal").

A proofwiki entry is available: https://proofwiki.org/wiki/Metric_Space_is_T4

(I cannot add [kind: wish] label to this issue. Perhaps because of the lack of permission?)

[affeldt-aist]

(I cannot add [kind: wish] label to this issue. Perhaps because of the lack of permission?)

There is maybe something to configure on github's side. I couldn't figure it out easily.

[affeldt-aist]

See this comment https://github.com/math-comp/analysis/blob/a6f5faaad30c89779f5e1c3bb70f530e69d5bb71/theories/topology.v#L5728-L5736

[affeldt-aist]

Since normal spaces have made their way into master we can maybe close this issues ? https://github.com/math-comp/analysis/blob/master/theories/topology.v#L427

[t6s]

Yes.