[isabelle-dev] New AFP entry Gromov Hyperbolicity in devel

Lawrence Paulson lp15 at cam.ac.uk
Thu Jan 18 12:45:29 CET 2018

I wonder whether some of this material should be moved to the Analysis library.

> On 18 Jan 2018, at 06:51, Tobias Nipkow <nipkow at in.tum.de> wrote:
> Along the way, we introduce basic material on isometries, quasi-isometries, Lipschitz maps, geodesic spaces, the Hausdorff distance, the Cauchy completion of a metric space, and the exponential on extended real numbers.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180118/60ca5276/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180118/60ca5276/attachment.sig>

More information about the isabelle-dev mailing list