[isabelle-dev] Gromov Hyperbolicity
eberlm at in.tum.de
Fri Jan 19 12:12:32 CET 2018
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
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev