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 inno
For those of you interested in formalization of Analysis
https://devel.isa-afp.org/entries/Gromov_Hyperbolicity.html
I would like to call your attention to this entry because it is rich in concepts
and theorems that are more general than the actual focus of the article. I
believe quite a bit o
Thanks for this discussion. Although I agree with Larry and Andreas, it is clear
that there is no concensus. Hence there will be no blanket change of where line
breaks go for infix operators.
Tobias
On 16/01/2018 17:34, Blanchette, J.C. wrote:
This sort of claim needs to be justified by evi
