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

I wonder whether some of this material should be moved to the Analysis library. Larry > On 18 Jan 2018, at 06:51, Tobias Nipkow wrote: > > Along the way, we introduce basic material on isometries, quasi-isometries, > Lipschitz maps, geodesic spaces, the Hausdorff distance,

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

We have a new AFP entry in the development branch of the AFP: Gromov Hyperbolicity Sebastien Gouezel A geodesic metric space is Gromov hyperbolic if all its geodesic triangles are thin, i.e., every side is contained in a fixed thickening of the two other sides. While this definition looks