[isabelle-dev] Gromov Hyperbolicity

[Manuel Eberl]

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, 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 cover Gödel's
>> theorem, which we would not want to move to our core libraries.
>>
>> Larry
>>
>>> On 18 Jan 2018, at 13:31, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>>
>>> It sounds like a reasonable criterion. Can you tell us what that
>>> means for Hausdorff_Distance, Metric_Completion and Isometries (as
>>> detailed by Fabian)?
>>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180118/1040fcb8/attachment-0002.html>