[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

analysis/theories/topology.v

Lines 5728 to 5736 in a6f5faa

	(* This section proves that uniform spaces, with a countable base for their
	entourage, are metrizable. The definition of this metric is rather arcane,
	and the proof is tough. That's ok because the resulting metric is not
	intended to be used explicitly. Instead, this is typically used in
	applications that do not depend on the metric:
	- `metric spaces are T4`
	- `in metric spaces, compactness and sequential compactness agree`
	- infinite products of metric spaces are metrizable
	*)

[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.