[isabelle-dev] Gromov Hyperbolicity

[Manuel Eberl]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180119/2865d4e4/attachment-0002.html>