CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> metric space (changes) in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="noindex,nofollow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> metric space (changes) </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/diff/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/3109/#Item_12" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <p class="show_diff"> Showing changes from revision #69 to #70: <ins class="diffins">Added</ins> | <del class="diffdel">Removed</del> | <del class="diffmod">Chan</del><ins class="diffmod">ged</ins> </p> <div class='rightHandSide'> <div class='toc clickDown' tabindex='0'> <h3 id='context'>Context</h3> <h4 id='analysis'>Analysis</h4> <div class='hide'> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/analysis'>analysis</a></strong> (<a class='existingWikiWord' href='/nlab/show/diff/differential+calculus'>differential</a>/<a class='existingWikiWord' href='/nlab/show/diff/integral+calculus'>integral</a> <a class='existingWikiWord' href='/nlab/show/diff/calculus'>calculus</a>, <a class='existingWikiWord' href='/nlab/show/diff/functional+analysis'>functional analysis</a>, <a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a>)</p> <p><a class='existingWikiWord' href='/nlab/show/diff/epsilontic+analysis'>epsilontic analysis</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/infinitesimal+analysis'>infinitesimal analysis</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/computable+analysis'>computable analysis</a></p> <p><em><a class='existingWikiWord' href='/nlab/show/diff/Introduction+to+Topology+--+1'>Introduction</a></em></p> <h2 id='basic_concepts'>Basic concepts</h2> <p><a class='existingWikiWord' href='/nlab/show/diff/triangle+inequality'>triangle inequality</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/metric+space'>metric space</a>, <a class='existingWikiWord' href='/nlab/show/diff/norm'>normed vector space</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/ball'>open ball</a>, <a class='existingWikiWord' href='/nlab/show/diff/open+subspace'>open subset</a>, <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhood</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/metric+topology'>metric topology</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequence</a>, <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/convergence'>convergence</a>, <a class='existingWikiWord' href='/nlab/show/diff/convergence'>limit of a sequence</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compactness</a>, <a class='existingWikiWord' href='/nlab/show/diff/sequentially+compact+topological+space'>sequential compactness</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/differentiation'>differentiation</a>, <a class='existingWikiWord' href='/nlab/show/diff/integral'>integration</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+vector+space'>topological vector space</a></p> <h2 id='basic_facts'>Basic facts</h2> <p><a class='existingWikiWord' href='/nlab/show/diff/continuous+metric+space+valued+function+on+compact+metric+space+is+uniformly+continuous'>continuous metric space valued function on compact metric space is uniformly continuous</a></p> <p>…</p> <h2 id='theorems'>Theorems</h2> <p><a class='existingWikiWord' href='/nlab/show/diff/intermediate+value+theorem'>intermediate value theorem</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/extreme+value+theorem'>extreme value theorem</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/Heine-Borel+theorem'>Heine-Borel theorem</a></p> <p>…</p> </div> </div> </div> <h1 id='contents'>Contents</h1> <div class='maruku_toc'><ul><li><a href='#idea'>Idea</a></li><li><a href='#definitions'>Definitions</a><ul><li><a href='#as_a_richman_premetric_space'>As a Richman premetric space</a></li><li><a href='#metrizable_spaces'>Metrizable spaces</a></li><li><a href='#variations'>Variations</a></li><li><a href='#metrics_valued_in_another_archimedean_integral_domain'>Metrics valued in another Archimedean integral domain</a></li><li><a href='#in_homotopy_type_theory'><span> In<del class='diffmod'> homotopy</del><ins class='diffmod'> dependent</ins> type theory</span></a></li><li><a href='#category_of_metric_spaces'>Category of metric spaces</a></li></ul></li><li><a href='#LawvereMetricSpace'>Lawvere metric spaces</a></li><li><a href='#motivation_for_the_axioms'>Motivation for the axioms</a></li><li><a href='#examples'>Examples</a></li><li><a href='#properties'>Properties</a></li><li><a href='#related_concepts'>Related concepts</a></li><li><a href='#references'>References</a></li></ul></div> <h2 id='idea'>Idea</h2> <p>A <strong>metric space</strong> is a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> which comes equipped with a <a class='existingWikiWord' href='/nlab/show/diff/function'>function</a> which measures <em>distance</em> between points, called a <em>metric</em>. The metric may be used to generate a <a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a> on the set, the <em><a class='existingWikiWord' href='/nlab/show/diff/metric+topology'>metric topology</a></em>, and a <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a> whose topology comes from some metric is said to be <em><a class='existingWikiWord' href='/nlab/show/diff/metrisable+topological+space'>metrizable</a></em>.</p> <h2 id='definitions'>Definitions</h2> <p>Traditionally, a <strong>metric space</strong> is defined to be a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_1' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> equipped with a <strong>distance</strong> <a class='existingWikiWord' href='/nlab/show/diff/function'>function</a></p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_2' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo lspace='verythinmathspace'>:</mo><mi>X</mi><mo>×</mo><mi>X</mi><mo>→</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>∞</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'> d\colon X \times X \to [0, \infty) </annotation></semantics></math></div> <p>(valued in <a class='existingWikiWord' href='/nlab/show/diff/positive+number'>non-negative</a> <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real numbers</a>) satisfying the following axioms:</p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/triangle+inequality'>Triangle inequality</a>: <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_3' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>+</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo><mo>≥</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>d(x, y) + d(y, z) \geq d(x, z)</annotation></semantics></math>;</p> </li> <li> <p>Point inequality: <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_4' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn><mo>≥</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>0 \geq d(x, x)</annotation></semantics></math> (so <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_5' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn><mo>=</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>0 = d(x,x)</annotation></semantics></math>);</p> </li> <li> <p>Separation: <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_6' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding='application/x-tex'>x = y</annotation></semantics></math> if <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_7' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x, y) = 0</annotation></semantics></math> (so <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_8' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding='application/x-tex'>x = y</annotation></semantics></math> iff <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_9' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x,y) = 0</annotation></semantics></math>);</p> </li> <li> <p>Symmetry: <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_10' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>d(x, y) = d(y, x)</annotation></semantics></math>.</p> </li> </ul> <p>Given a metric space <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_11' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>d</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X, d)</annotation></semantics></math> and a point <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_12' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>x \in X</annotation></semantics></math>, the <strong><a class='existingWikiWord' href='/nlab/show/diff/ball'>open ball</a></strong> centered at <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_13' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> of radius <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_14' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>r</mi></mrow><annotation encoding='application/x-tex'>r</annotation></semantics></math> is</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_15' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>B</mi> <mi>r</mi></msub><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>≔</mo><mo stretchy='false'>{</mo><mi>y</mi><mo>∈</mo><mi>X</mi><mo>:</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo><</mo><mi>r</mi><mo stretchy='false'>}</mo></mrow><annotation encoding='application/x-tex'> B_r(x) \coloneqq \{y \in X : d(x, y) \lt r\} </annotation></semantics></math></div> <p>and it may be shown that the open balls form a <a class='existingWikiWord' href='/nlab/show/diff/topological+base'>basis</a> for a <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topology</a> on <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_16' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>, the <em><a class='existingWikiWord' href='/nlab/show/diff/metric+topology'>metric topology</a></em>. In fact, metric spaces are examples of <a class='existingWikiWord' href='/nlab/show/diff/uniform+space'>uniform spaces</a>, and much of the general theory of metric spaces, including for example the notion of <a class='existingWikiWord' href='/nlab/show/diff/complete+space'>completion</a> of a metric space, can be extrapolated to uniform spaces and even <a class='existingWikiWord' href='/nlab/show/diff/Cauchy+space'>Cauchy spaces</a>.</p> <h3 id='as_a_richman_premetric_space'>As a Richman premetric space</h3> <p>In <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a>, a <strong>metric space</strong> is a <a class='existingWikiWord' href='/nlab/show/diff/Richman+premetric+space'>Richman premetric space</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_17' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mo>∼</mo><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X, \sim)</annotation></semantics></math> such that for all non-negative rational numbers <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_18' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>q</mi><mo>∈</mo><msub><mi>ℚ</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub></mrow><annotation encoding='application/x-tex'>q \in \mathbb{Q}_{\geq 0}</annotation></semantics></math>, and <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_19' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>r</mi><mo>∈</mo><msub><mi>ℚ</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub></mrow><annotation encoding='application/x-tex'>r \in \mathbb{Q}_{\geq 0}</annotation></semantics></math>, if <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_20' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>q</mi><mo><</mo><mi>r</mi></mrow><annotation encoding='application/x-tex'>q \lt r</annotation></semantics></math>, than for every <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_21' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>x \in X</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_22' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi><mo>∈</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>y \in X</annotation></semantics></math>, either <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_23' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><msub><mo>∼</mo> <mi>r</mi></msub><mi>y</mi></mrow><annotation encoding='application/x-tex'>x \sim_r y</annotation></semantics></math> or <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_24' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>¬</mo><mo stretchy='false'>(</mo><mi>x</mi><msub><mo>∼</mo> <mi>q</mi></msub><mi>y</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\neg(x \sim_q y)</annotation></semantics></math>. Classically, every Richman premetric space is a metric space, but constructively, Richman premetric spaces are only “metric spaces” that are valued in the lower Dedekind real numbers.</p> <h3 id='metrizable_spaces'>Metrizable spaces</h3> <p>A <strong><a class='existingWikiWord' href='/nlab/show/diff/metrisable+topological+space'>metrizable topological space</a></strong> is a <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_25' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> which admits a metric such that the <a class='existingWikiWord' href='/nlab/show/diff/metric+topology'>metric topology</a> agrees with the topology on <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_26' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>. In general, many different metrics (even ones giving different <a class='existingWikiWord' href='/nlab/show/diff/uniform+space'>uniform structures</a>) may give rise to the same topology; nevertheless, metrizability is manifestly a topological notion.</p> <p>Metrizable spaces enjoy a number of separation properties: they are <a class='existingWikiWord' href='/nlab/show/diff/Hausdorff+space'>Hausdorff</a>, <a class='existingWikiWord' href='/nlab/show/diff/regular+space'>regular</a>, and even <a class='existingWikiWord' href='/nlab/show/diff/normal+space'>normal</a>. They are also <a class='existingWikiWord' href='/nlab/show/diff/paracompact+topological+space'>paracompact</a>.</p> <p>Metrizable spaces are closed under topological <a class='existingWikiWord' href='/nlab/show/diff/coproduct'>coproducts</a> and of course <a class='existingWikiWord' href='/nlab/show/diff/subspace'>subspaces</a> (and therefore <a class='existingWikiWord' href='/nlab/show/diff/equalizer'>equalizers</a>); they are closed under <a class='existingWikiWord' href='/nlab/show/diff/countable+set'>countable</a> <a class='existingWikiWord' href='/nlab/show/diff/cartesian+product'>products</a> but not general products (for instance, a product of uncountably many copies of the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_27' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{R}</annotation></semantics></math> is not a normal space).</p> <p>Fundamental early work in point-set topology established a number of metrization theorems, i.e., theorems which give sufficient conditions for a space to be metrizable. One of the more useful theorems is due to <a class='existingWikiWord' href='/nlab/show/diff/Pavel+Urysohn'>Urysohn</a>:</p> <p>\begin{theorem}\label{UrysohnMetrizationTheorem} <strong>(<a class='existingWikiWord' href='/nlab/show/diff/Urysohn+metrization+theorem'>Urysohn metrization theorem</a>)</strong> \linebreak A <a class='existingWikiWord' href='/nlab/show/diff/separation+axioms'>regular, Hausdorff</a> <a class='existingWikiWord' href='/nlab/show/diff/second-countable+space'>second-countable space</a> is metrizable. \end{theorem}</p> <p>\begin{example} A <a class='existingWikiWord' href='/nlab/show/diff/compactum'>compact Hausdorff space</a> that is second-countable is metrizable. \end{example}</p> <p>\begin{remark} <strong>(<a class='existingWikiWord' href='/nlab/show/diff/counterexample'>counter-example</a>)</strong> \linebreak A <a class='existingWikiWord' href='/nlab/show/diff/compactum'>compact Hausdorff space</a> that is merely <a class='existingWikiWord' href='/nlab/show/diff/separable+space'>separable</a> need not be metrizable.</p> <p>One <a class='existingWikiWord' href='/nlab/show/diff/counterexample'>counter-example</a> is the <a class='existingWikiWord' href='/nlab/show/diff/Stone-%C4%8Cech+compactification'>Stone-Cech compactification</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_28' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo stretchy='false'>(</mo><mi>ℕ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\beta(\mathbb{N})</annotation></semantics></math>, in which the <a class='existingWikiWord' href='/nlab/show/diff/discrete+and+indiscrete+topology'>discrete space</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_29' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{N}</annotation></semantics></math> of <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a> is <a class='existingWikiWord' href='/nlab/show/diff/dense+subspace'>dense</a>, whle no non-principal <a class='existingWikiWord' href='/nlab/show/diff/ultrafilter'>ultrafilter</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_30' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> is the <a class='existingWikiWord' href='/nlab/show/diff/convergence'>limit of a sequence</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_31' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi><mo>=</mo><mo stretchy='false'>{</mo><msub><mi>x</mi> <mi>n</mi></msub><mo stretchy='false'>}</mo><mo>⊆</mo><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>X = \{x_n\} \subseteq \mathbb{N}</annotation></semantics></math> of principal ultrafilters.</p> <p>Namely: Supposing it were, choose complementary subsets <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_32' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>,</mo><mi>B</mi><mo>⊆</mo><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>A, B \subseteq \mathbb{N}</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_33' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>∩</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>A \cap X</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_34' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi><mo>∩</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>B \cap X</annotation></semantics></math> are infinite. By the decomposition <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_35' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo stretchy='false'>(</mo><mi>ℕ</mi><mo stretchy='false'>)</mo><mo>=</mo><mi>β</mi><mo stretchy='false'>(</mo><mi>A</mi><mo>+</mo><mi>B</mi><mo stretchy='false'>)</mo><mo>=</mo><mi>β</mi><mo stretchy='false'>(</mo><mi>A</mi><mo stretchy='false'>)</mo><mo>+</mo><mi>β</mi><mo stretchy='false'>(</mo><mi>B</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\beta(\mathbb{N}) = \beta(A + B) = \beta(A) + \beta(B)</annotation></semantics></math>, we have <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_36' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> belonging to exactly one of <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_37' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo stretchy='false'>(</mo><mi>A</mi><mo stretchy='false'>)</mo><mo>,</mo><mi>β</mi><mo stretchy='false'>(</mo><mi>B</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\beta(A), \beta(B)</annotation></semantics></math>, say <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_38' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo stretchy='false'>(</mo><mi>B</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\beta(B)</annotation></semantics></math>. But since the subsequence <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_39' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>∩</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>A \cap X</annotation></semantics></math> converges to <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_40' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math>, the basic open neighborhood <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_41' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo stretchy='false'>(</mo><mi>B</mi><mo stretchy='false'>)</mo><mo>=</mo><mo stretchy='false'>{</mo><mi>V</mi><mo>∈</mo><mi>β</mi><mo stretchy='false'>(</mo><mi>ℕ</mi><mo stretchy='false'>)</mo><mo>:</mo><mi>B</mi><mo>∈</mo><mi>V</mi><mo stretchy='false'>}</mo></mrow><annotation encoding='application/x-tex'>\beta(B) = \{V \in \beta(\mathbb{N}): B \in V\}</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_42' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> intersects <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_43' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>∩</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>A \cap X</annotation></semantics></math> non-trivially, i.e., <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_44' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> is contained in some principal ultrafilter <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_45' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>prin</mi><mo stretchy='false'>(</mo><mi>a</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>prin(a)</annotation></semantics></math> with <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_46' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi><mo>∩</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>a \in A \cap X</annotation></semantics></math>. Then <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_47' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi></mrow><annotation encoding='application/x-tex'>a</annotation></semantics></math> lies in disjoint sets <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_48' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_49' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>∩</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>A \cap X</annotation></semantics></math>, contradiction. \end{remark}</p> <h3 id='variations'>Variations</h3> <p>If we allow <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_50' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi></mrow><annotation encoding='application/x-tex'>d</annotation></semantics></math> to take values in <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_51' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>∞</mn><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[0,\infty]</annotation></semantics></math> (the nonnegative <a class='existingWikiWord' href='/nlab/show/diff/one-sided+real+number'>lower reals</a>) instead of just in <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_52' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>∞</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>[0,\infty)</annotation></semantics></math>, then we get <strong>extended metric spaces</strong>. If we drop separation, then we get <strong>pseudometric spaces</strong>. If we drop the symmetry condition, then we get <strong>quasimetric spaces</strong>. Thus the most general notion is that of an extended quasipseudometric space, which are also called <strong>Lawvere metric spaces</strong> for the reasons below.</p> <p id='LawvereMetricSpacesDefinition'>On the other hand, if we strengthen the <a class='existingWikiWord' href='/nlab/show/diff/triangle+inequality'>triangle inequality</a> to</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_53' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>max</mi><mo stretchy='false'>(</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>,</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo><mo stretchy='false'>)</mo><mo>≥</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo><mo>,</mo></mrow><annotation encoding='application/x-tex'> max(d(x,y), d(y,z)) \geq d(x,z) ,</annotation></semantics></math></div> <p>then we get <strong>ultrametric spaces</strong>, a more restricted concept. (This include for example <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_54' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi></mrow><annotation encoding='application/x-tex'>p</annotation></semantics></math>-<a class='existingWikiWord' href='/nlab/show/diff/formal+completion'>adic completion</a>s of <a class='existingWikiWord' href='/nlab/show/diff/number+field'>number fields</a>.) Extended quasipseudoultrametric spaces can also be called <strong>Lawvere ultrametric spaces</strong>.</p> <h3 id='metrics_valued_in_another_archimedean_integral_domain'>Metrics valued in another Archimedean integral domain</h3> <p>In some cases, we might want our <a class='existingWikiWord' href='/nlab/show/diff/target'>codomain</a> of our metric to take values in values other than the real numbers <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_55' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{R}</annotation></semantics></math>. This is already important in the definition of the real numbers as <a class='existingWikiWord' href='/nlab/show/diff/Cauchy+real+number'>modulated Cauchy real numbers</a>, where the metric used is valued in the <a class='existingWikiWord' href='/nlab/show/diff/positive+number'>non-negative</a> <a class='existingWikiWord' href='/nlab/show/diff/rational+number'>rational numbers</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_56' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ℚ</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub></mrow><annotation encoding='application/x-tex'>\mathbb{Q}_{\geq 0}</annotation></semantics></math>.</p> <p>This becomes even more essential in <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a>: while in <a class='existingWikiWord' href='/nlab/show/diff/classical+mathematics'>classical mathematics</a>, the <a class='existingWikiWord' href='/nlab/show/diff/Cauchy+real+number'>modulated Cauchy real numbers</a> are equivalent to the <a class='existingWikiWord' href='/nlab/show/diff/Dedekind+cut'>Dedekind real numbers</a>, in <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a>, those definitions are inequivalent to the <a class='existingWikiWord' href='/nlab/show/diff/Dedekind+cut'>Dedekind real numbers</a>, and so there are multiple sets of real numbers in which a metric could be valued in. Something similar happens in <a class='existingWikiWord' href='/nlab/show/diff/predicative+mathematics'>predicative</a> <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a> with the <a class='existingWikiWord' href='/nlab/show/diff/subset+collection'>axiom of fullness</a>: the Dedekind real numbers could be defined as <a class='existingWikiWord' href='/nlab/show/diff/Cauchy+real+number'>multivalued Cauchy real numbers</a>, which is unique up to field isomorphism.</p> <p>In <a class='existingWikiWord' href='/nlab/show/diff/predicative+mathematics'>predicative</a> <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a> without the <a class='existingWikiWord' href='/nlab/show/diff/subset+collection'>axiom of fullness</a>, the issue becomes even worse: there is no longer one set of Dedekind real numbers. In some <a class='existingWikiWord' href='/nlab/show/diff/foundation+of+mathematics'>foundations</a>, there is a whole hierarchy of Dedekind real numbers, one set for every <a class='existingWikiWord' href='/nlab/show/diff/universe'>universe</a> in the foundations. In other foundations, there isn’t even a single set of Dedekind real numbers. As a result, one cannot resort to merely using the <a class='existingWikiWord' href='/nlab/show/diff/Dedekind+cut'>Dedekind real numbers</a> for defining the metric as in impredicative mathematics, one has to define metrics and metric spaces more generally.</p> <p>Thus, given an <a class='existingWikiWord' href='/nlab/show/diff/Archimedean+ordered+integral+domain'>Archimedean integral domain</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_57' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>R</mi></mrow><annotation encoding='application/x-tex'>R</annotation></semantics></math>, an <strong><math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_58' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>R</mi></mrow><annotation encoding='application/x-tex'>R</annotation></semantics></math>-metric</strong> on a set <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_59' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> is a function <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_60' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo>:</mo><mi>X</mi><mo>×</mo><mi>X</mi><mo>→</mo><msub><mi>R</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub></mrow><annotation encoding='application/x-tex'>d:X \times X \to R_{\geq 0}</annotation></semantics></math>, where <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_61' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>R</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub></mrow><annotation encoding='application/x-tex'>R_{\geq 0}</annotation></semantics></math> is the set of non-negative elements in <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_62' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>R</mi></mrow><annotation encoding='application/x-tex'>R</annotation></semantics></math>, such that</p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/triangle+inequality'>Triangle inequality</a>: <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_63' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>+</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo><mo>≥</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>d(x, y) + d(y, z) \geq d(x, z)</annotation></semantics></math>;</p> </li> <li> <p>Point inequality: <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_64' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn><mo>≥</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>0 \geq d(x, x)</annotation></semantics></math> (so <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_65' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn><mo>=</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>0 = d(x,x)</annotation></semantics></math>);</p> </li> <li> <p>Separation: <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_66' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding='application/x-tex'>x = y</annotation></semantics></math> if <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_67' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x, y) = 0</annotation></semantics></math> (so <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_68' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding='application/x-tex'>x = y</annotation></semantics></math> iff <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_69' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x,y) = 0</annotation></semantics></math>);</p> </li> <li> <p>Symmetry: <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_70' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>d(x, y) = d(y, x)</annotation></semantics></math>.</p> </li> </ul> <p>This is equivalently an <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_71' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>R</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub><mo>,</mo><mo>≥</mo><mo>,</mo><mo lspace='verythinmathspace' rspace='0em'>+</mo><mo>,</mo><mn>0</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(R_{\geq 0}, \geq, +, 0)</annotation></semantics></math>-<a class='existingWikiWord' href='/nlab/show/diff/enriched+set'>enriched set</a>.</p> <p>Given any <a class='existingWikiWord' href='/nlab/show/diff/Archimedean+ordered+integral+domain'>Archimedean integral domain</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_72' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>R</mi></mrow><annotation encoding='application/x-tex'>R</annotation></semantics></math> and an Archimedean integral subdomain <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_73' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>⊆</mo><mi>R</mi></mrow><annotation encoding='application/x-tex'>S \subseteq R</annotation></semantics></math>, then <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_74' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is an <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_75' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>R</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub><mo>,</mo><mo>≥</mo><mo>,</mo><mo lspace='verythinmathspace' rspace='0em'>+</mo><mo>,</mo><mn>0</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(R_{\geq 0}, \geq, +, 0)</annotation></semantics></math>-enriched set.</p> <h3 id='in_homotopy_type_theory'><span> In<del class='diffmod'> homotopy</del><ins class='diffmod'> dependent</ins> type theory</span></h3> <p>In <a class='existingWikiWord' href='/nlab/show/diff/homotopy+type+theory'><span><del class='diffmod'> homotopy</del><ins class='diffmod'> dependent</ins> type theory</span></a>, metric and pseudometric spaces could be defined as any <a class='existingWikiWord' href='/nlab/show/diff/type'>type</a>, not just 0-truncated types. Let <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_76' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{R}</annotation></semantics></math> be some suitable notion of real number, and</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_77' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ℝ</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub><mo>≔</mo><munder><mo lspace='thinmathspace' rspace='thinmathspace'>∑</mo> <mrow><mi>a</mi><mo>:</mo><mi>ℝ</mi></mrow></munder><mi>a</mi><mo>≥</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>\mathbb{R}_{\geq 0} \coloneqq \sum_{a:\mathbb{R}} a \geq 0</annotation></semantics></math></div> <p>be the non-negative real numbers.</p> <p>\begin{definition} A <strong>pseudometric space</strong> is a type <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_78' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> with a function <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_79' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo>:</mo><mi>X</mi><mo>×</mo><mi>X</mi><mo>→</mo><msub><mi>ℝ</mi> <mrow><mo>≥</mo><mn>0</mn></mrow></msub></mrow><annotation encoding='application/x-tex'>d:X \times X \to \mathbb{R}_{\geq 0}</annotation></semantics></math>, which comes with witnesses for symmetry, the triangle identity, and the identity-to-zero-distance condition:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_80' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi mathvariant='normal'>sym</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>:</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\mathrm{sym}(x, y):d(x, y) = d(y, x)</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_81' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi mathvariant='normal'>triangle</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo><mo>:</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo><mo>≤</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>+</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\mathrm{triangle}(x, y, z):d(x, z) \leq d(x, y) + d(y, z)</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_82' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi mathvariant='normal'>idtozerodis</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>:</mo><mo stretchy='false'>(</mo><mi>x</mi><mo>=</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>→</mo><mo stretchy='false'>(</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\mathrm{idtozerodis}(x, y):(x = y) \to (d(x, y) = 0)</annotation></semantics></math></div> <p>\end{definition}</p> <p>The last axiom is equivalent to the point inequality axiom</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_83' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi mathvariant='normal'>ptineq</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>:</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>\mathrm{ptineq}(x):d(x, x) = 0</annotation></semantics></math></div> <p>by the induction principle of <a class='existingWikiWord' href='/nlab/show/diff/identity+type'>identity types</a>. Every pseudometric can be shown to have an <a class='existingWikiWord' href='/nlab/show/diff/equivalence+relation'>equivalence relation</a></p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_84' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∼</mo><mi>y</mi><mo>≔</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>x \sim y \coloneqq d(x, y) = 0</annotation></semantics></math></div> <p>through the axioms of a pseudometric space.</p> <p>In set theory, the separation axiom is usually defined as the converse of the identity-to-zero-distance axiom. However, in type theory, since not all identity types are propositions, merely postulating a function</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_85' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi mathvariant='normal'>sepax</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>:</mo><mo stretchy='false'>(</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn><mo stretchy='false'>)</mo><mo>→</mo><mo stretchy='false'>(</mo><mi>x</mi><mo>=</mo><mi>y</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\mathrm{sepax}(x, y):(d(x, y) = 0) \to (x = y)</annotation></semantics></math></div> <p>does not result in a metric space, since there might be many such functions into the identity type <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_86' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding='application/x-tex'>x = y</annotation></semantics></math>. Instead, one must strengthen the condition to a <a class='existingWikiWord' href='/nlab/show/diff/Rezk+completion'>Rezk completeness</a> condition for pseudometric spaces, similar to the type-theoretic antisymmetry condition in <a class='existingWikiWord' href='/nlab/show/diff/partial+order'>posets</a> from <a class='existingWikiWord' href='/nlab/show/diff/preorder'>preordered types</a>:</p> <p>\begin{definition} A pseudometric space is a <strong>metric space</strong> if the axiom</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_87' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi mathvariant='normal'>idtozerodis</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>:</mo><mo stretchy='false'>(</mo><mi>x</mi><mo>=</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>→</mo><mo stretchy='false'>(</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\mathrm{idtozerodis}(x, y):(x = y) \to (d(x, y) = 0)</annotation></semantics></math></div> <p>is an <a class='existingWikiWord' href='/nlab/show/diff/equivalence+of+types'>equivalence of types</a>. \end{definition}</p> <p>Since any type of non-negative real numbers is a set, the Rezk completeness condition automatically implies that every metric space is a set.</p> <h3 id='category_of_metric_spaces'>Category of metric spaces</h3> <p>When working with metric spaces one encounters a broad variety of different maps including non-<a class='existingWikiWord' href='/nlab/show/diff/continuous+map'>continuous</a> ones like almost isometries. For a convenient categorical set-up one often restricts to <strong><a class='existingWikiWord' href='/nlab/show/diff/short+map'>short maps</a></strong>, i.e. maps that do not increase any distance or, equivalently, have are of <a class='existingWikiWord' href='/nlab/show/diff/Lipschitz+map'>Lipschitz norm</a> not greater than 1. The category of Lawvere metric spaces and short maps forms the <a class='existingWikiWord' href='/nlab/show/diff/short+map'>category of metric spaces</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_88' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Met</mi></mrow><annotation encoding='application/x-tex'>Met</annotation></semantics></math>. The restriction to ordinary metric spaces is denoted by <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_89' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>Met</mi> <mi>ord</mi></msub></mrow><annotation encoding='application/x-tex'>Met_{ord}</annotation></semantics></math>.</p> <h2 id='LawvereMetricSpace'>Lawvere metric spaces</h2> <p>In <a href='#Lawvere73'>Lawvere, 73</a>, it was pointed out that <a href='#LawvereMetricSpacesDefinition'>Lawvere metric spaces</a> are precisely <a class='existingWikiWord' href='/nlab/show/diff/enriched+category'>categories enriched</a> in the <a class='existingWikiWord' href='/nlab/show/diff/monoidal+category'>monoidal</a> <a class='existingWikiWord' href='/nlab/show/diff/partial+order'>poset</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_90' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>∞</mn><mo stretchy='false'>]</mo><mo>,</mo><mo>≥</mo><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>([0, \infty], \geq)</annotation></semantics></math>, where the <a class='existingWikiWord' href='/nlab/show/diff/tensor+product'>tensor product</a> is taken to be addition. The <a class='existingWikiWord' href='/nlab/show/diff/composition'>composition</a> operation in this enriched category identifies with the <a class='existingWikiWord' href='/nlab/show/diff/triangle+identities'>triangle identity</a> in the metric space (see at <em><a href='triangle+inequality#InterpretationInEnrichedCategoryTheory'>triangle inequality – Interpretation in enriched category theory</a></em>).</p> <p>Alternatively, taking the monoidal product to be <a class='existingWikiWord' href='/nlab/show/diff/join'>supremum</a> instead, enriched categories amount to Lawvere ultrametric spaces.</p> <p>Thus generalized, many constructions and results on metric spaces turn out to be special cases of yet more general constructions and results of <a class='existingWikiWord' href='/nlab/show/diff/enriched+category+theory'>enriched category theory</a>. This includes for example the notion of <a class='existingWikiWord' href='/nlab/show/diff/Cauchy+complete+category'>Cauchy completion</a>, which in general enriched category theory is related to <a class='existingWikiWord' href='/nlab/show/diff/Karoubi+envelope'>Karoubi envelopes</a> and <a class='existingWikiWord' href='/nlab/show/diff/Morita+equivalence'>Morita equivalence</a>.</p> <p>Imposing the symmetry axiom then gives us enriched <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_91' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>†</mo></mrow><annotation encoding='application/x-tex'>\dagger</annotation></semantics></math>-<a class='existingWikiWord' href='/nlab/show/diff/dagger+category'>categories</a>. Note that when enriching over a <a class='existingWikiWord' href='/nlab/show/diff/cartesian+monoidal+category'>cartesian monoidal</a> poset, there is no difference between a <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_92' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>†</mo></mrow><annotation encoding='application/x-tex'>\dagger</annotation></semantics></math>-category and a <a class='existingWikiWord' href='/nlab/show/diff/groupoid'>groupoid</a>, so ultrametric spaces can also be regarded as <a class='existingWikiWord' href='/nlab/show/diff/enriched+groupoid'>enriched groupoids</a>, which is perhaps a more familiar concept.</p> <p>(The requisite axioms for an enriched groupoid do not make sense when the enriching category is not cartesian, but one might argue that since in a poset “they would commute automatically anyway”, it makes sense to call any poset-enriched <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_93' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>†</mo></mrow><annotation encoding='application/x-tex'>\dagger</annotation></semantics></math>-category also an “enriched groupoid”. However, perhaps it makes more sense just to speak about enriched <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_94' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>†</mo></mrow><annotation encoding='application/x-tex'>\dagger</annotation></semantics></math>-categories.)</p> <p>In the presence of the symmetry axiom, the “separation” axiom “<math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_95' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding='application/x-tex'>x=y</annotation></semantics></math> if <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_96' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x,y)=0</annotation></semantics></math>” is equivalent to <a class='existingWikiWord' href='/nlab/show/diff/skeleton'>skeletality</a> of an enriched category. That is, a pseudo-metric space is a metric space precisely when it is skeletal. But in the non-symmetric case, this separation axiom is stronger than skeletality; the latter would say only “<math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_97' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding='application/x-tex'>x=y</annotation></semantics></math> if <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_98' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x,y)=d(y,x)=0</annotation></semantics></math>”. That is, a quasi-pseudo-metric space can be skeletal without being a quasi-metric space, at least the way the latter term is usually used.</p> <p>Note that like any kind of enriched category, Lawvere metric spaces are <a class='existingWikiWord' href='/nlab/show/diff/monad'>monads</a> in a <a class='existingWikiWord' href='/nlab/show/diff/bicategory'>bicategory</a> of “matrices”, whose objects are sets and whose morphisms from <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_99' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> to <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_100' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Y</mi></mrow><annotation encoding='application/x-tex'>Y</annotation></semantics></math> are functions <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_101' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo>:</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo>→</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>∞</mn><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>d:X\times Y \to [0,\infty]</annotation></semantics></math>. This sort of perspective can be generalized to many other kinds of topological structures; an exposition can be found in the book <a href='#HST'>Monoidal topology</a>.</p> <p>The category of metric spaces and categories of random maps as generalised metric spaces were studied in the <a href='#Meng'>thesis</a> of Lawvere’s student Xiao-qing Meng.</p> <h2 id='motivation_for_the_axioms'>Motivation for the axioms</h2> <p>The <a class='existingWikiWord' href='/nlab/show/diff/triangle+inequality'>triangle axiom</a> is the fundamental idea behind a metric space; it goes back (at least) to <a class='existingWikiWord' href='/nlab/show/diff/Euclid'>Euclid</a> and captures the idea that we are discussing the <em>shortest</em> distance between two points. Given the triangle inequality, we have the polygon inequality</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_102' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>0</mn></msub><mo>,</mo><msub><mi>x</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo><mo>+</mo><mi>⋯</mi><mo>+</mo><mi>d</mi><mo stretchy='false'>(</mo><msub><mi>x</mi> <mrow><mi>n</mi><mo>−</mo><mn>1</mn></mrow></msub><mo>,</mo><msub><mi>x</mi> <mi>n</mi></msub><mo stretchy='false'>)</mo><mo>≥</mo><mi>d</mi><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>0</mn></msub><mo>,</mo><msub><mi>x</mi> <mi>n</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'> d(x_0,x_1) + \cdots + d(x_{n-1},x_n) \geq d(x_0,x_n) </annotation></semantics></math></div> <p>for all <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_103' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>n</mi><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>n \gt 0</annotation></semantics></math>; the point inequality extends this to <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_104' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>n</mi><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>n = 0</annotation></semantics></math>.</p> <p>Besides extended metric spaces (where distances may be infinite), one might consider spaces where distances may be negative. But in fact this gives us nothing new, at least if we have symmetry. First,</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_105' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>+</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>≥</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'> d(x,x) + d(x,x) \geq d(x,x) </annotation></semantics></math></div> <p>forces <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_106' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>≥</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x,x) \geq 0</annotation></semantics></math>, so <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_107' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x,x) = 0</annotation></semantics></math>; then</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_108' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>+</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>≥</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'> 2 d(x,y) = d(x,y) + d(y,x) \geq d(x,x) </annotation></semantics></math></div> <p>forces <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_109' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>≥</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x,y) \geq 0</annotation></semantics></math>. A generalisation to negative distances is possible for quasimetric spaces, however; the simplest example has <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_110' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn></mrow><annotation encoding='application/x-tex'>2</annotation></semantics></math> elements, with <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_111' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mo lspace='verythinmathspace' rspace='0em'>−</mo><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>d(x,y) = -d(y,x)</annotation></semantics></math> (but necessarily <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_112' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>d(x,x) = 0</annotation></semantics></math> still).</p> <p>We can define a <a class='existingWikiWord' href='/nlab/show/diff/preorder'>preorder</a> <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_113' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>≤</mo></mrow><annotation encoding='application/x-tex'>\leq</annotation></semantics></math> on the points of a Lawvere metric space:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_114' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi><mspace width='thickmathspace' /><mo>⇔</mo><mspace width='thickmathspace' /><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn><mo>.</mo></mrow><annotation encoding='application/x-tex'> x \leq y \;\Leftrightarrow\; d(x,y) = 0 .</annotation></semantics></math></div> <p>Then the symmetry axiom implies that this relation is <a class='existingWikiWord' href='/nlab/show/diff/symmetric+relation'>symmetric</a> and hence an <a class='existingWikiWord' href='/nlab/show/diff/equivalence+relation'>equivalence relation</a>. The <a class='existingWikiWord' href='/nlab/show/diff/quotient+set'>quotient set</a> under this equivalence relation satisfies separation; in this way, every pseudometric space is <a class='existingWikiWord' href='/nlab/show/diff/equivalence+of+categories'>equivalent</a> (as an enriched category) to a metric space. Even for quasimetric spaces, we can still define an equivalence relation:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_115' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>≡</mo><mi>y</mi><mspace width='thickmathspace' /><mo>⇔</mo><mspace width='thickmathspace' /><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn><mspace width='thickmathspace' /><mo>∧</mo><mspace width='thickmathspace' /><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn><mo>.</mo></mrow><annotation encoding='application/x-tex'> x \equiv y \;\Leftrightarrow\; d(x,y) = 0 \;\wedge\; d(y,x) = 0 .</annotation></semantics></math></div> <p>In <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a>, it works better to use <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_116' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>⪇</mo></mrow><annotation encoding='application/x-tex'>\lneq</annotation></semantics></math>:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_117' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>⪇</mo><mi>y</mi><mspace width='thickmathspace' /><mo>⇔</mo><mspace width='thickmathspace' /><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn><mo>;</mo></mrow><annotation encoding='application/x-tex'> x \lneq y \;\Leftrightarrow\; d(x,y) \gt 0 ;</annotation></semantics></math></div> <p>then the symmetry axiom implies that this is an <a class='existingWikiWord' href='/nlab/show/diff/apartness+relation'>apartness relation</a>, which (for quasimetric spaces) we can also define directly:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_118' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>#</mo><mi>y</mi><mspace width='thickmathspace' /><mo>⇔</mo><mspace width='thickmathspace' /><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn><mspace width='thickmathspace' /><mo>∨</mo><mspace width='thickmathspace' /><mi>d</mi><mo stretchy='false'>(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn><mo>.</mo></mrow><annotation encoding='application/x-tex'> x \# y \;\Leftrightarrow\; d(x,y) \gt 0 \;\vee\; d(y,x) \gt 0 .</annotation></semantics></math></div> <h2 id='examples'>Examples</h2> <ul> <li> <p>Every <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> carries the <strong><a class='existingWikiWord' href='/nlab/show/diff/discrete+object'>discrete metric</a></strong> given by</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_119' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>≔</mo><mrow><mo>{</mo><mrow><mtable><mtr><mtd><mn>0</mn></mtd> <mtd><mtext>if </mtext><mi>x</mi><mo>=</mo><mi>y</mi></mtd></mtr> <mtr><mtd><mn>1</mn></mtd> <mtd><mtext>otherwise</mtext></mtd></mtr></mtable></mrow></mrow></mrow><annotation encoding='application/x-tex'> d(x,y) \coloneqq \left\{\array{ 0 & \text{if } x = y \\ 1 & \text{otherwise} }\right. </annotation></semantics></math></div> <p>For certain purposes, it makes more sense to make most the non-zero distance <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_120' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>∞</mn></mrow><annotation encoding='application/x-tex'>\infty</annotation></semantics></math> instead of <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_121' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>1</mn></mrow><annotation encoding='application/x-tex'>1</annotation></semantics></math>; then one has an extended metric space.</p> </li> <li> <p>Every <a class='existingWikiWord' href='/nlab/show/diff/norm'>normed vector space</a> is a metric space by <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_122' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>≔</mo><mrow><mo stretchy='false'>‖</mo><mi>x</mi><mo>−</mo><mi>y</mi><mo stretchy='false'>‖</mo></mrow></mrow><annotation encoding='application/x-tex'>d(x,y) \coloneqq {\|x - y\|}</annotation></semantics></math>; a pseudonormed vector space is a pseudometric space.</p> </li> <li> <p>Every <a class='existingWikiWord' href='/nlab/show/diff/connected+space'>connected</a> <a class='existingWikiWord' href='/nlab/show/diff/Riemannian+manifold'>Riemannian manifold</a> becomes a pseudometric space (or a metric space if, as is often assumed, the manifold is <a class='existingWikiWord' href='/nlab/show/diff/Hausdorff+space'>Hausdorff</a>) by taking the distance between two points to be <a class='existingWikiWord' href='/nlab/show/diff/meet'>infimum</a> of the Riemannian lengths of all continuously differentiable <a class='existingWikiWord' href='/nlab/show/diff/path'>paths</a> connecting them:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_123' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>d</mi><mo stretchy='false'>(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>≔</mo><msub><mi>inf</mi> <mrow><mi>x</mi><mover><mo>→</mo><mi>γ</mi></mover><mi>y</mi></mrow></msub><mi>len</mi><mo stretchy='false'>(</mo><mi>γ</mi><mo stretchy='false'>)</mo><mo>.</mo></mrow><annotation encoding='application/x-tex'> d(x,y) \coloneqq inf_{x \stackrel{\gamma}{\to} y} len(\gamma) . </annotation></semantics></math></div> <p>If the manifold might not be connected, then it still becomes an extended metric space.</p> </li> </ul> <h2 id='properties'>Properties</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Lebesgue+number+lemma'>Lebesgue number lemma</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/sequentially+compact+metric+spaces+are+totally+bounded'>sequentially compact metric spaces are totally bounded</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/sequentially+compact+metric+spaces+are+equivalently+compact+metric+spaces'>sequentially compact metric spaces are equivalently compact metric spaces</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/countably+compact+metric+spaces+are+equivalently+compact+metric+spaces'>countably compact metric spaces are equivalently compact metric spaces</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/metric+spaces+are+fully+normal'>metric spaces are fully normal</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/metric+spaces+are+paracompact'>metric spaces are paracompact</a></p> </li> </ul> <h2 id='related_concepts'>Related concepts</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/induced+metric'>induced metric</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/metric+jet'>metric jet</a> – a notion of “tangency” for maps of metric spaces</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/complete+space'>complete metric space</a> and <a class='existingWikiWord' href='/nlab/show/diff/localic+completion'>localic completion</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/separable+metric+space'>separable metric space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/distance+%28graph+theory%29'>distance (graph theory)</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Booij+premetric+space'>Booij premetric space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Richman+premetric+space'>Richman premetric space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/enriched+preorder'>enriched poset</a></p> </li> </ul> <p><strong>Generalized uniform structures</strong></p> <table><thead><tr><th><a class='existingWikiWord' href='/nlab/show/diff/2-category+equipped+with+proarrows'>proarrow</a></th><th><a class='existingWikiWord' href='/nlab/show/diff/monad'>monad</a></th><th><a class='existingWikiWord' href='/nlab/show/diff/Rezk+completion'>Rezk-complete</a> version</th><th><a class='existingWikiWord' href='/nlab/show/diff/pro-object'>pro</a>-monad</th><th>symmetric versions</th><th /><th /><th /></tr></thead><tbody><tr><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/relation'>binary relation</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/preorder'>preorder</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/partial+order'>partial order</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/uniform+space'>quasiuniformity</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/symmetric+relation'>symmetric relation</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/equivalence+relation'>equivalence relation</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/equality'>equality</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/uniform+space'>uniformity</a></td></tr> <tr><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/binary+function'>binary function</a> to <math class='maruku-mathml' display='inline' id='mathml_9ead9fe878cad6546b34db9696ee0c792d94ffc6_124' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>∞</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>[0,\infty)</annotation></semantics></math></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/metric+space'>quasipseudometric</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/metric+space'>quasimetric</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/prometric+space'>quasiprometric</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/binary+function'>symmetric binary function</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/metric+space'>pseudometric</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/metric+space'>metric</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/prometric+space'>prometric</a></td></tr> <tr><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/proximity+space'>topogeny</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/proximity+space'>quasiproximity</a></td><td style='text-align: left;' /><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/syntopogenous+space'>syntopogeny</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/proximity+space'>symmetric topogeny</a></td><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/proximity+space'>proximity</a></td><td style='text-align: left;' /><td style='text-align: left;'><a class='existingWikiWord' href='/nlab/show/diff/syntopogenous+space'>symmetric syntopogeny</a></td></tr> </tbody></table> <h2 id='references'>References</h2> <ul> <li> <p>Wikipedia, <em><a href='https://en.wikipedia.org/wiki/Metric_space'>Metric space</a></em></p> </li> <li id='Lawvere73'> <p><a class='existingWikiWord' href='/nlab/show/diff/William+Lawvere'>Bill Lawvere</a> (1973). <em>Metric spaces, generalized logic and closed categories</em>. Reprinted in <a class='existingWikiWord' href='/nlab/show/diff/Theory+and+Applications+of+Categories'>TAC</a>, 1986. <a href='http://www.tac.mta.ca/tac/reprints/articles/1/tr1abs.html'>Web</a>.</p> </li> <li id='Meng'> <p>Xiao-qing Meng, <em>Categories of convex sets and of metric spaces with applications to stochastic programming and related areas</em>, PhD thesis (<a class='existingWikiWord' href='/nlab/files/Meng.djvu' title='Ph.D. thesis of Meng'>djvu</a>)</p> </li> <li id='HST'> <p>Dirk Hofmann, Gavin J. Seal, and Walter Tholen (editors), <em>Monoidal topology: A Categorical Approach to Order, Metric, and Topology</em>, Cambridge University Press, 2014</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Fred+Richman'>Fred Richman</a>, <em>Real numbers and other completions</em>, Mathematical Logic Quarterly <strong>54</strong> 1 (2008) 98-108 [[doi:10.1002/malq.200710024](https://onlinelibrary.wiley.com/doi/10.1002/malq.200710024)]</p> </li> <li> <p>Auke B. Booij, Analysis in univalent type theory (<a href='https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf'>pdf</a>)</p> </li> </ul> <p> </p> <p> </p> </div> <div class="revisedby"> <p> Last revised on November 13, 2024 at 22:04:05. See the <a href="/nlab/history/metric+space" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/metric+space" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/3109/#Item_12">Discuss</a><span class="backintime"><a href="/nlab/revision/diff/metric+space/69" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/metric+space" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Hide changes</a><a href="/nlab/history/metric+space" accesskey="S" class="navlink" id="history" rel="nofollow">History (69 revisions)</a> <a href="/nlab/show/metric+space/cite" style="color: black">Cite</a> <a href="/nlab/print/metric+space" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/metric+space" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>