Metric pseudocompletion of pseudometric spaces

[malarbol]

(WIP)

• pseudometric completions of a pseudometric spaceM: the pseudometric space of Cauchy approximations in M where two Cauchy approximations x and y are in a d-neighborhood of one another if for all δ ε : ℚ⁺, x δ and y ε are in a (δ + ε + d)-neighborhood of one another in M;

• metric quotients of a pseudometric space M: the metric space whose points are quotient classes of M by the similarity relation and neighborhoods given by neighborhoods of inhabitants of the quotient classes: two quotient classes X, Y are in a d-neighborhood if for all x ∈ X and y ∈ Y, x and y are d-neighbors in the pseudometric space.

• [...]

Co-authored-by: Louis Wasserman [email protected]

[malarbol]

Some work towards #1458

[malarbol]

Closing this as it is dealt with in #1618 #1619 #1622 etc.