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 before.
Lipschitz continuity is certainly undergraduate material. That probably appears in any introductory Analysis lecture, even those for computer scientists. Manuel On 2018-01-19 12:01, Tjark Weber wrote: > 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 Isometries (as detailed by Fabian)? > Metric completion features prominently, e.g., in the construction of > the reals. Lipschitz continuity (along with the Picard–Lindelöf > theorem) should be part of any course on differential equations. > > I can't recall whether I've been taught about Hausdorff distance or > even isometries during my undergraduate years. Of course, these are > fairly simple concepts. > > Best, > Tjark > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
