[isabelle-dev] Gromov Hyperbolicity

[Tjark Weber]

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