Re: [isabelle-dev] Gromov Hyperbolicity

I'm afraid I've no idea. I didn't study much analysis for my first degree, not even the basics of complex analysis. Larry > On 18 Jan 2018, at 14:29, Tobias Nipkow wrote: > > So what is the situation wrt the theories I asked about?

Re: [isabelle-dev] Gromov Hyperbolicity

I for one have not encountered any of these things in my undergraduate mathematics lectures. But the situation may well be different in other universities. On 2018-01-18 15:29, Tobias Nipkow wrote: > So what is the situation wrt the theories I asked about? > > Tobias > > On 18/01/2018 15:11,

Re: [isabelle-dev] Gromov Hyperbolicity

So what is the situation wrt the theories I asked about? Tobias On 18/01/2018 15:11, Lawrence Paulson wrote: This is mainly a negative criterion, i.e., something outside the undergraduate curriculum probably should not be in our core libraries. But I would guess for example mathematicians

Re: [isabelle-dev] Gromov Hyperbolicity

This is mainly a negative criterion, i.e., something outside the undergraduate curriculum probably should not be in our core libraries. But I would guess for example mathematicians cover Gödel's theorem, which we would not want to move to our core libraries. Larry > On 18 Jan 2018, at 13:31,

Re: [isabelle-dev] Gromov Hyperbolicity

> Am 18.01.2018 um 14:36 schrieb Tobias Nipkow : > > > > On 18/01/2018 11:06, Fabian Immler wrote: >>> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow : >>> >>> 1. Library/Complement contains both new generic material like "t3_space" >>> but also new

Re: [isabelle-dev] Gromov Hyperbolicity

On 18/01/2018 11:06, Fabian Immler wrote: Am 18.01.2018 um 08:32 schrieb Tobias Nipkow : 1. Library/Complement contains both new generic material like "t3_space" but also new concepts like [mono_intros] for more automation in proving of inequalities. In short, there is a

Re: [isabelle-dev] Gromov Hyperbolicity

On 18/01/2018 12:48, Lawrence Paulson wrote: We certainly need to solve this problem. Absolutely. For practical reasons I would put as much in the AFP as possible, (One could make exceptions for small theories, but this could get out of hand again). One possible criterion: which results

Re: [isabelle-dev] Gromov Hyperbolicity

We certainly need to solve this problem. One possible criterion: which results are part of a standard undergraduate athematics curriculum? Larry > On 18 Jan 2018, at 10:06, Fabian Immler wrote: > > We do not have a precise specification of what HOL-Analysis is or should be.

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,

Re: [isabelle-dev] Gromov Hyperbolicity

> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow : > > 1. Library/Complement contains both new generic material like "t3_space" but > also new concepts like [mono_intros] for more automation in proving of > inequalities. In short, there is a wealth of material that might be