<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p><font size="+1">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.<br>
</font></p>
<p><font size="+1">Lipschitz continuity is certainly undergraduate
material. That probably appears in any introductory Analysis
lecture, even those for computer scientists.</font></p>
<p><font size="+1">Manuel<br>
</font></p>
<br>
<div class="moz-cite-prefix">On 2018-01-19 12:01, Tjark Weber wrote:<br>
</div>
<blockquote type="cite" cite="mid:1516359696.1556.13.camel@it.uu.se">
<pre wrap="">On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote:
</pre>
<blockquote type="cite">
<blockquote type="cite">
<pre wrap="">One possible criterion: which results
are part of a standard undergraduate athematics curriculum?
</pre>
</blockquote>
<pre wrap="">
It sounds like a reasonable criterion. Can you tell us what that means for
Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?
</pre>
</blockquote>
<pre wrap="">
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
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>