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 before.
Lipschitz continuity is certainly undergraduate material. That probably
appears in any introductory Analysis lecture, even those for computer
scientists.
Manuel
On 2018-01-19 12:01, Tjark Weber wrote:
> 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 Isometries (as detailed by Fabian)?
> Metric completion features prominently, e.g., in the construction of
> the reals. Lipschitz continuity (along with the Picard–Lindelöf
> theorem) should be part of any course on differential equations.
>
> I can't recall whether I've been taught about Hausdorff distance or
> even isometries during my undergraduate years. Of course, these are
> fairly simple concepts.
>
> Best,
> Tjark
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
