Refactor metric spaces

[malarbol]

Refactoring the metric space module (#1421)

• remove the notion of Premetric / Premetric-Space;
• all (pseudo)metric spaces are saturated;
• simplify hierarchy in concepts (define things for for metric spaces first, instead of the splitting premetric>pseudometric>metric);

[malarbol]

I'm opening this for review to have some feedback although it's obviously not ready to be merged.
This intends to be a first step towards #1421 and set up a new name scheme / hierarchy for metric spaces. The current content should act as replacement for the following modules:

• metric-spaces.closed-premetric-structures
• metric-spaces.extensional-premetric-structures
• metric-spaces.metric-spaces
• metric-spaces.metric-structures
• metric-spaces.monotonic-premetric-structures
• metric-spaces.premetric-spaces
• metric-spaces.premetric-structures
• metric-spaces.pseudometric-spaces
• metric-spaces.pseudometric-structures
• metric-spaces.reflexive-premetric-structures
• metric-spaces.saturated-metric-spaces
• metric-spaces.symmetric-premetric-structures
• metric-spaces.triangular-premetric-structures

A lot of modules will need to be updated to follow this new scheme so I'd rather have these first definitions right before going further in the refactoring.

[malarbol]

Some more work towards #1421, refactoring morphisms (isometries, short maps, uniformly continuous maps, continuous maps) for the new name scheme.

I've been thinking that, even though these concepts can be defined in terms of rational neighborhoods relations, they're mostly inserting in the (pseudo)metric cases and the whole hierarchy premetric>pseudometric>metric (e.g. for short maps, isometries, etc.) was a bit too much. So it's probably simpler to define them for metric spaces first, then if we need it, transpose the concepts for pseudometric spaces (I still hope we can do without Type-With-Rational-Neighborhood-Relation).

The last few patches should replace the following modules:

• metric-spaces.continuous-functions-metric-spaces
• metric-spaces.isometries-metric-spaces
• metric-spaces.isometries-premetric-spaces
• metric-spaces.short-functions-metric-spaces
• metric-spaces.short-functions-premetric-spaces
• metric-spaces.uniformly-continuous-functions-metric-spaces
• metric-spaces.uniformly-continuous-functions-premetric-spaces