Oh, well, yes, a special case of metric completion (the reals) was
mentioned in passing, I think. And a more general notion (something like
the completion of a topological group, I think?) featured in my Algebra
1 course, which was an elective. But "metric completion" as such I have
not heard
On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote:
> > One possible criterion: which results
> > are part of a standard undergraduate athematics curriculum?
>
> It sounds like a reasonable criterion. Can you tell us what that means for
> Hausdorff_Distance, Metric_Completion and
