Re: [isabelle-dev] Gromov Hyperbolicity

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

Re: [isabelle-dev] Gromov Hyperbolicity

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

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] 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

[isabelle-dev] Gromov Hyperbolicity

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