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
