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> net (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> net (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/11009/#Item_2" 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 #38 to #39: <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='topology'>Topology</h4> <div class='hide'> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a></strong> (<a class='existingWikiWord' href='/nlab/show/diff/general+topology'>point-set topology</a>, <a class='existingWikiWord' href='/nlab/show/diff/point-free+topology'>point-free topology</a>)</p> <p>see also <em><a class='existingWikiWord' href='/nlab/show/diff/differential+topology'>differential topology</a></em>, <em><a class='existingWikiWord' href='/nlab/show/diff/algebraic+topology'>algebraic topology</a></em>, <em><a class='existingWikiWord' href='/nlab/show/diff/functional+analysis'>functional analysis</a></em> and <em><a class='existingWikiWord' href='/nlab/show/diff/topological+homotopy+theory'>topological</a> <a class='existingWikiWord' href='/nlab/show/diff/homotopy+theory'>homotopy theory</a></em></p> <p><a class='existingWikiWord' href='/nlab/show/diff/Introduction+to+Topology'>Introduction</a></p> <p><strong>Basic concepts</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/open+subspace'>open subset</a>, <a class='existingWikiWord' href='/nlab/show/diff/closed+subspace'>closed subset</a>, <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhood</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a>, <a class='existingWikiWord' href='/nlab/show/diff/locale'>locale</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+base'>base for the topology</a>, <a class='existingWikiWord' href='/nlab/show/diff/neighborhood+base'>neighbourhood base</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/finer+topology'>finer/coarser topology</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/closed+subspace'>closure</a>, <a class='existingWikiWord' href='/nlab/show/diff/interior'>interior</a>, <a class='existingWikiWord' href='/nlab/show/diff/boundary'>boundary</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/separation+axioms'>separation</a>, <a class='existingWikiWord' href='/nlab/show/diff/sober+topological+space'>sobriety</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/continuous+map'>continuous function</a>, <a class='existingWikiWord' href='/nlab/show/diff/homeomorphism'>homeomorphism</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/uniformly+continuous+map'>uniformly continuous function</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/embedding+of+topological+spaces'>embedding</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/open+map'>open map</a>, <a class='existingWikiWord' href='/nlab/show/diff/closed+map'>closed map</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequence</a>, <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a>, <a class='existingWikiWord' href='/nlab/show/diff/subnet'>sub-net</a>, <a class='existingWikiWord' href='/nlab/show/diff/filter'>filter</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/convergence'>convergence</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/category'>category</a> <a class='existingWikiWord' href='/nlab/show/diff/Top'>Top</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/convenient+category+of+topological+spaces'>convenient category of topological spaces</a></li> </ul> </li> </ul> <p><strong><a href='Top#UniversalConstructions'>Universal constructions</a></strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/weak+topology'>initial topology</a>, <a class='existingWikiWord' href='/nlab/show/diff/weak+topology'>final topology</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/subspace'>subspace</a>, <a class='existingWikiWord' href='/nlab/show/diff/quotient+space'>quotient space</a>,</p> </li> <li> <p>fiber space, <a class='existingWikiWord' href='/nlab/show/diff/space+attachment'>space attachment</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/product+topological+space'>product space</a>, <a class='existingWikiWord' href='/nlab/show/diff/disjoint+union+topological+space'>disjoint union space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/mapping+cylinder'>mapping cylinder</a>, <a class='existingWikiWord' href='/nlab/show/diff/cocylinder'>mapping cocylinder</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/mapping+cone'>mapping cone</a>, <a class='existingWikiWord' href='/nlab/show/diff/mapping+cocone'>mapping cocone</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/mapping+telescope'>mapping telescope</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/colimits+of+normal+spaces'>colimits of normal spaces</a></p> </li> </ul> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/stuff%2C+structure%2C+property'>Extra stuff, structure, properties</a></strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/nice+topological+space'>nice topological space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/metric+space'>metric space</a>, <a class='existingWikiWord' href='/nlab/show/diff/metric+topology'>metric topology</a>, <a class='existingWikiWord' href='/nlab/show/diff/metrisable+topological+space'>metrisable space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Kolmogorov+topological+space'>Kolmogorov space</a>, <a class='existingWikiWord' href='/nlab/show/diff/Hausdorff+space'>Hausdorff space</a>, <a class='existingWikiWord' href='/nlab/show/diff/regular+space'>regular space</a>, <a class='existingWikiWord' href='/nlab/show/diff/normal+space'>normal space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/sober+topological+space'>sober space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compact space</a>, <a class='existingWikiWord' href='/nlab/show/diff/proper+map'>proper map</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/sequentially+compact+topological+space'>sequentially compact</a>, <a class='existingWikiWord' href='/nlab/show/diff/countably+compact+topological+space'>countably compact</a>, <a class='existingWikiWord' href='/nlab/show/diff/locally+compact+topological+space'>locally compact</a>, <a class='existingWikiWord' href='/nlab/show/diff/sigma-compact+topological+space'>sigma-compact</a>, <a class='existingWikiWord' href='/nlab/show/diff/paracompact+topological+space'>paracompact</a>, <a class='existingWikiWord' href='/nlab/show/diff/countably+paracompact+topological+space'>countably paracompact</a>, <a class='existingWikiWord' href='/nlab/show/diff/strongly+compact+topological+space'>strongly compact</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/compactly+generated+topological+space'>compactly generated space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/second-countable+space'>second-countable space</a>, <a class='existingWikiWord' href='/nlab/show/diff/first-countable+space'>first-countable space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/contractible+space'>contractible space</a>, <a class='existingWikiWord' href='/nlab/show/diff/locally+contractible+space'>locally contractible space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/connected+space'>connected space</a>, <a class='existingWikiWord' href='/nlab/show/diff/locally+connected+topological+space'>locally connected space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/simply+connected+space'>simply-connected space</a>, <a class='existingWikiWord' href='/nlab/show/diff/semi-locally+simply-connected+topological+space'>locally simply-connected space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/cell+complex'>cell complex</a>, <a class='existingWikiWord' href='/nlab/show/diff/CW+complex'>CW-complex</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/pointed+topological+space'>pointed space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+vector+space'>topological vector space</a>, <a class='existingWikiWord' href='/nlab/show/diff/Banach+space'>Banach space</a>, <a class='existingWikiWord' href='/nlab/show/diff/Hilbert+space'>Hilbert space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+group'>topological group</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+vector+bundle'>topological vector bundle</a>, <a class='existingWikiWord' href='/nlab/show/diff/topological+K-theory'>topological K-theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+manifold'>topological manifold</a></p> </li> </ul> <p><strong>Examples</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/empty+space'>empty space</a>, <a class='existingWikiWord' href='/nlab/show/diff/point+space'>point space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/discrete+object'>discrete space</a>, <a class='existingWikiWord' href='/nlab/show/diff/codiscrete+space'>codiscrete space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Sierpinski+space'>Sierpinski space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/order+topology'>order topology</a>, <a class='existingWikiWord' href='/nlab/show/diff/specialization+topology'>specialization topology</a>, <a class='existingWikiWord' href='/nlab/show/diff/Scott+topology'>Scott topology</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Euclidean+space'>Euclidean space</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a>, <a class='existingWikiWord' href='/nlab/show/diff/plane'>plane</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/cylinder+object'>cylinder</a>, <a class='existingWikiWord' href='/nlab/show/diff/cone'>cone</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/sphere'>sphere</a>, <a class='existingWikiWord' href='/nlab/show/diff/ball'>ball</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/circle'>circle</a>, <a class='existingWikiWord' href='/nlab/show/diff/torus'>torus</a>, <a class='existingWikiWord' href='/nlab/show/diff/annulus'>annulus</a>, <a class='existingWikiWord' href='/nlab/show/diff/M%C3%B6bius+strip'>Moebius strip</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/polytope'>polytope</a>, <a class='existingWikiWord' href='/nlab/show/diff/polyhedron'>polyhedron</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/projective+space'>projective space</a> (<a class='existingWikiWord' href='/nlab/show/diff/real+projective+space'>real</a>, <a class='existingWikiWord' href='/nlab/show/diff/complex+projective+space'>complex</a>)</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/classifying+space'>classifying space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/configuration+space+of+points'>configuration space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/path'>path</a>, <a class='existingWikiWord' href='/nlab/show/diff/loop'>loop</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/compact-open+topology'>mapping spaces</a>: <a class='existingWikiWord' href='/nlab/show/diff/compact-open+topology'>compact-open topology</a>, <a class='existingWikiWord' href='/nlab/show/diff/topology+of+uniform+convergence'>topology of uniform convergence</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/loop+space'>loop space</a>, <a class='existingWikiWord' href='/nlab/show/diff/path+space'>path space</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Zariski+topology'>Zariski topology</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Cantor+space'>Cantor space</a>, <a class='existingWikiWord' href='/nlab/show/diff/Mandelbrot+set'>Mandelbrot space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Peano+curve'>Peano curve</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/line+with+two+origins'>line with two origins</a>, <a class='existingWikiWord' href='/nlab/show/diff/long+line'>long line</a>, <a class='existingWikiWord' href='/nlab/show/diff/Sorgenfrey+line'>Sorgenfrey line</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/K-topology'>K-topology</a>, <a class='existingWikiWord' href='/nlab/show/diff/Dowker+space'>Dowker space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Warsaw+circle'>Warsaw circle</a>, <a class='existingWikiWord' href='/nlab/show/diff/Hawaiian+earring+space'>Hawaiian earring space</a></p> </li> </ul> <p><strong>Basic statements</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Hausdorff+implies+sober'>Hausdorff spaces are sober</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/schemes+are+sober'>schemes are sober</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/continuous+images+of+compact+spaces+are+compact'>continuous images of compact spaces are compact</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/closed+subspaces+of+compact+Hausdorff+spaces+are+equivalently+compact+subspaces'>closed subspaces of compact Hausdorff spaces are equivalently compact subspaces</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/open+subspaces+of+compact+Hausdorff+spaces+are+locally+compact'>open subspaces of compact Hausdorff spaces are locally compact</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/quotient+projections+out+of+compact+Hausdorff+spaces+are+closed+precisely+if+the+codomain+is+Hausdorff'>quotient projections out of compact Hausdorff spaces are closed precisely if the codomain is Hausdorff</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/compact+spaces+equivalently+have+converging+subnets'>compact spaces equivalently have converging subnet of every net</a></p> <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+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/compact+spaces+equivalently+have+converging+subnets'>compact spaces equivalently have converging subnet of every net</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> </ul> </li> <li> <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> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/paracompact+Hausdorff+spaces+are+normal'>paracompact Hausdorff spaces are normal</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/paracompact+Hausdorff+spaces+equivalently+admit+subordinate+partitions+of+unity'>paracompact Hausdorff spaces equivalently admit subordinate partitions of unity</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/closed+injections+are+embeddings'>closed injections are embeddings</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/proper+maps+to+locally+compact+spaces+are+closed'>proper maps to locally compact spaces are closed</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/injective+proper+maps+to+locally+compact+spaces+are+equivalently+the+closed+embeddings'>injective proper maps to locally compact spaces are equivalently the closed embeddings</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/locally+compact+and+sigma-compact+spaces+are+paracompact'>locally compact and sigma-compact spaces are paracompact</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/locally+compact+and+second-countable+spaces+are+sigma-compact'>locally compact and second-countable spaces are sigma-compact</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/second-countable+regular+spaces+are+paracompact'>second-countable regular spaces are paracompact</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/CW-complexes+are+paracompact+Hausdorff+spaces'>CW-complexes are paracompact Hausdorff spaces</a></p> </li> </ul> <p><strong>Theorems</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Urysohn%27s+lemma'>Urysohn's lemma</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Tietze+extension+theorem'>Tietze extension theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Tychonoff+theorem'>Tychonoff theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/tube+lemma'>tube lemma</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Michael%27s+theorem'>Michael's theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Brouwer%27s+fixed+point+theorem'>Brouwer's fixed point theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+invariance+of+dimension'>topological invariance of dimension</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Jordan+curve+theorem'>Jordan curve theorem</a></p> </li> </ul> <p><strong>Analysis Theorems</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Heine-Borel+theorem'>Heine-Borel theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/intermediate+value+theorem'>intermediate value theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/extreme+value+theorem'>extreme value theorem</a></p> </li> </ul> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/topological+homotopy+theory'>topological homotopy theory</a></strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/homotopy'>left homotopy</a>, <a class='existingWikiWord' href='/nlab/show/diff/homotopy'>right homotopy</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/homotopy+equivalence'>homotopy equivalence</a>, <a class='existingWikiWord' href='/nlab/show/diff/deformation+retract'>deformation retract</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/fundamental+group'>fundamental group</a>, <a class='existingWikiWord' href='/nlab/show/diff/covering+space'>covering space</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/fundamental+theorem+of+covering+spaces'>fundamental theorem of covering spaces</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/homotopy+group'>homotopy group</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/weak+homotopy+equivalence'>weak homotopy equivalence</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Whitehead+theorem'>Whitehead's theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Freudenthal+suspension+theorem'>Freudenthal suspension theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/nerve+theorem'>nerve theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/homotopy+extension+property'>homotopy extension property</a>, <a class='existingWikiWord' href='/nlab/show/diff/Hurewicz+cofibration'>Hurewicz cofibration</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+cofiber+sequence'>cofiber sequence</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Str%C3%B8m+model+structure'>Strøm model category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/classical+model+structure+on+topological+spaces'>classical model structure on topological spaces</a></p> </li> </ul> </div> <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='#DirectedSets'>Directed sets</a></li><li><a href='#Nets'>Nets</a></li><li><a href='#subnets'>Subnets</a></li><li><a href='#NetsAndFilters'>Eventuality filters</a></li></ul></li><li><a href='#properties'>Properties</a><ul><li><a href='#RelationToTopology'>Relation to topology</a></li><li><a href='#LogicOfNets'>Logic of nets</a></li></ul></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 <em>net</em> in a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_1' 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 <a class='existingWikiWord' href='/nlab/show/diff/function'>function</a> from a <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_2' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>D</mi></mrow><annotation encoding='application/x-tex'>D</annotation></semantics></math> to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_3' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>. Special cases of nets are <a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequences</a>, for which <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_4' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>D</mi><mo>=</mo><msub><mi>ℕ</mi> <mo>≤</mo></msub></mrow><annotation encoding='application/x-tex'>D = \mathbb{N}_{\leq}</annotation></semantics></math> is the <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a>. Regarded as a generalization of sequences, nets are used in <a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a> for formalization of the concept of <a class='existingWikiWord' href='/nlab/show/diff/convergence'>convergence</a>.</p> <p>Nets are also called <em>Moore–Smith sequences</em> and are equivalent (in a certain sense) to <a class='existingWikiWord' href='/nlab/show/diff/filter'>proper filters</a> (def. <a class='maruku-ref' href='#Filter'>8</a> below), their <em><a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filters</a></em> (def. <a class='maruku-ref' href='#EventualityFilter'>9</a> below).</p> <p>The concept of nets is motivated from the fact that where plain <a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequences</a> detect <a class='existingWikiWord' href='/nlab/show/diff/topology'>topological</a> properties in <a class='existingWikiWord' href='/nlab/show/diff/metric+space'>metric spaces</a>, in generally they fail to do so in more general <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological spaces</a>. For example <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>, but for general <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological spaces</a> being <a class='existingWikiWord' href='/nlab/show/diff/sequentially+compact+topological+space'>sequentially compact</a> neither implies nor is implied by being <a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compact</a> (see at <em><a class='existingWikiWord' href='/nlab/show/diff/sequentially+compact+topological+space'>sequentially compact space</a></em> <a href='sequentially+compact+topological+space#Examples'>Examples and counter-examples</a>).</p> <p>Inspection of these counter-examples reveals that the problem is that sequences indexed by the <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a> may be “too short” in that they cannot go deep enough into uncountable territory, and they are “too slim” in that they proceed to their potential limiting point only from one direction, instead of from many at once. The use of general <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed sets</a> for nets in place of just the <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a> for sequences fixes these two issues.</p> <p>And indeed, as opposed to sequences, nets do detect</p> <ol> <li> <p>the topology on general topological spaces (prop. <a class='maruku-ref' href='#TopologyDetectedByNets'>2</a> below),</p> </li> <li> <p>the continuity of functions between them (prop. <a class='maruku-ref' href='#ContinuousFunctionsDetectedByNets'>3</a> below),</p> </li> <li> <p>the <a class='existingWikiWord' href='/nlab/show/diff/Hausdorff+space'>Hausdorff</a> property (prop. <a class='maruku-ref' href='#NetsDetectHausdorff'>4</a> below),</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compactness</a> (prop. <a class='maruku-ref' href='#CompactSpacesEquivalentlyHaveConvergetSubnets'>5</a> below).</p> </li> </ol> <p>While the concept of nets is similar to that of sequences, one gets a cleaner theory still by considering not the nets themselves but their “<a class='existingWikiWord' href='/nlab/show/diff/filter'>filters</a> of <a class='existingWikiWord' href='/nlab/show/diff/subset'>subsets</a> which they eventually meet” (def. <a class='maruku-ref' href='#EventuallyAndFrequently'>3</a> below), called their <em><a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filters</a></em> (def. <a class='maruku-ref' href='#EventualityFilter'>9</a> below). For example equivalent filters are equal (in contrast to nets) and (unless in <a class='existingWikiWord' href='/nlab/show/diff/predicative+mathematics'>predicative mathematics</a>) the set of filters on a set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_5' 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 class='existingWikiWord' href='/nlab/show/diff/small+set'>small</a> (not a proper class).</p> <h2 id='definitions'>Definitions</h2> <h3 id='DirectedSets'>Directed sets</h3> <div class='num_defn' id='DirectedSet'> <h6 id='definition'>Definition</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a>)</strong></p> <p>A <em><a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a></em> is</p> <ul> <li>a <a class='existingWikiWord' href='/nlab/show/diff/preorder'>preordered set</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_6' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>D</mi><mo>,</mo><mo>≤</mo><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(D, \leq)</annotation></semantics></math>, hence a set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_7' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>D</mi></mrow><annotation encoding='application/x-tex'>D</annotation></semantics></math> equipped with a <a class='existingWikiWord' href='/nlab/show/diff/reflexive+relation'>reflexive</a> and <a class='existingWikiWord' href='/nlab/show/diff/transitive+action'>transitive</a> <a class='existingWikiWord' href='/nlab/show/diff/relation'>relation</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_8' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>≤</mo></mrow><annotation encoding='application/x-tex'>\leq</annotation></semantics></math></li> </ul> <p>such that</p> <ul> <li>every <a class='existingWikiWord' href='/nlab/show/diff/finite+set'>finite</a> <a class='existingWikiWord' href='/nlab/show/diff/subset'>subset</a> has an <a class='existingWikiWord' href='/nlab/show/diff/upper+bound'>upper bound</a>, hence for any <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_9' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>∈</mo><mi>D</mi></mrow><annotation encoding='application/x-tex'>a,b \in D</annotation></semantics></math> there exists <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_10' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi><mo>∈</mo><mi>D</mi></mrow><annotation encoding='application/x-tex'>c \in D</annotation></semantics></math> with <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_11' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>≤</mo><mi>c</mi></mrow><annotation encoding='application/x-tex'>a \leq c</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_12' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>b</mi><mo>≤</mo><mi>c</mi></mrow><annotation encoding='application/x-tex'>b \leq c</annotation></semantics></math>.</li> </ul> </div> <div class='num_example' id='DirectedSetOfNaturalNumbers'> <h6 id='example'>Example</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a> of <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a>)</strong></p> <p>The <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_13' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{N}</annotation></semantics></math> with their canonical lower-or-equal relation <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_14' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>≤</mo></mrow><annotation encoding='application/x-tex'>\leq</annotation></semantics></math> form a <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a> (def. <a class='maruku-ref' href='#DirectedSet'>1</a>).</p> </div> <p>The key class of examples of nets, underlying their relation to <a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a> (<a href='#RelationToTopology'>below</a>) is the following:</p> <div class='num_example' id='DirectedSetOfNeighbourhods'> <h6 id='example_2'>Example</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a> of <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhoods</a>)</strong></p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_15' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X, \tau)</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a> and let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_16' 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> be an element of the underlying set. Then then set of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_17' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><mi>x</mi><msub><mo stretchy='false'>)</mo> <mo>⊃</mo></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(Nbhd_X(x)_{\supset})</annotation></semantics></math> <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhoods</a> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_18' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, ordered by <em>reverse</em> inclusion, is a <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a> (def. <a class='maruku-ref' href='#DirectedSet'>1</a>).</p> </div> <div class='num_example' id='DirectedProductSet'> <h6 id='example_3'>Example</h6> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_19' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>A</mi> <mo>≥</mo></msub></mrow><annotation encoding='application/x-tex'>A_{\geq}</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_20' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>B</mi> <mo>≥</mo></msub></mrow><annotation encoding='application/x-tex'>B_{\geq}</annotation></semantics></math> be two <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed sets</a> (def. <a class='maruku-ref' href='#DirectedSet'>1</a>). Then the <a class='existingWikiWord' href='/nlab/show/diff/cartesian+product'>Cartesian product</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_21' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>A \times B</annotation></semantics></math> of the underlying sets becomes itself a directed set by setting</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_22' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mo>(</mo><mo stretchy='false'>(</mo><msub><mi>a</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>b</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo><mo>≤</mo><mo stretchy='false'>(</mo><msub><mi>a</mi> <mn>2</mn></msub><mo>,</mo><msub><mi>b</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo><mo>)</mo></mrow><mspace width='thinmathspace' /><mo>≔</mo><mspace width='thinmathspace' /><mrow><mo>(</mo><mrow><mo>(</mo><msub><mi>a</mi> <mn>1</mn></msub><mo>≤</mo><msub><mi>a</mi> <mn>2</mn></msub><mo>)</mo></mrow><mspace width='thinmathspace' /><mtext>and</mtext><mspace width='thinmathspace' /><mrow><mo>(</mo><msub><mi>b</mi> <mn>1</mn></msub><mo>≤</mo><msub><mi>b</mi> <mn>2</mn></msub><mo>)</mo></mrow><mo>)</mo></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> \left( (a_1, b_1) \leq (a_2, b_2) \right) \,\coloneqq\, \left( \left( a_1 \leq a_2\right) \,\text{and}\, \left( b_1 \leq b_2 \right) \right) \,. </annotation></semantics></math></div></div> <h3 id='Nets'>Nets</h3> <div class='num_defn' id='Net'> <h6 id='definition_2'>Definition</h6> <p>For <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_23' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a>, then a <em>net</em> in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_24' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> is</p> <ol> <li> <p>a <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_25' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> (def. <a class='maruku-ref' href='#DirectedSet'>1</a>), called the <em>index set</em>,</p> </li> <li> <p>a <a class='existingWikiWord' href='/nlab/show/diff/function'>function</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_26' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> from (the underlying set of) <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_27' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_28' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>.</p> </li> </ol> <p>We say that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_29' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> <em>indexes</em> the net.</p> </div> <div class='num_example' id='SequencesAreNets'> <h6 id='example_4'>Example</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequences</a> are <a class='existingWikiWord' href='/nlab/show/diff/net'>nets</a>)</strong></p> <p>A <a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequence</a> is a net (def. <a class='maruku-ref' href='#Net'>2</a>) whose directed set of indices is the <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_30' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>ℕ</mi><mo>,</mo><mo>≤</mo><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(\mathbb{N}, \leq)</annotation></semantics></math> (example <a class='maruku-ref' href='#DirectedSetOfNaturalNumbers'>1</a>).</p> </div> <div class='num_remark'> <h6 id='remark'>Remark</h6> <p>Although the index set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_31' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> in def. <a class='maruku-ref' href='#Net'>2</a>, being a <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a>, is equipped with a <a class='existingWikiWord' href='/nlab/show/diff/preorder'>preorder</a>, the function <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_32' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> is not required to preserve this in any way. This forms an exception to the rule of thumb that a preordered set may be replaced by its quotient <a class='existingWikiWord' href='/nlab/show/diff/partial+order'>poset</a>.</p> <p>You can get around this if you instead define a net in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_33' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> as a <a class='existingWikiWord' href='/nlab/show/diff/multi-valued+function'>multi-valued function</a> from a partially ordered directed set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_34' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_35' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>. Although there is not much point to doing this in general, it can make a difference if you put restrictions on the possibilities for <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_36' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math>, in particular if you consider the definition of <a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequence</a>. In some <a class='existingWikiWord' href='/nlab/show/diff/type+theory'>type-theoretic</a> <a class='existingWikiWord' href='/nlab/show/diff/foundation+of+mathematics'>foundations</a> of mathematics, you can get the same effect by defining a net to be an ‘operation’ (a <a class='existingWikiWord' href='/nlab/show/diff/prefunction'>prefunction</a>, like a function but not required to preserve <a class='existingWikiWord' href='/nlab/show/diff/equality'>equality</a>). On the other hand, every net with domain <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_37' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> is equivalent (in the sense of having the same <a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filter</a>) to a net with domain <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_38' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi><mo>×</mo><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>A \times \mathbb{N}</annotation></semantics></math>, made into a partial order by defining <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_39' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>a</mi><mo>,</mo><mi>m</mi><mo stretchy='false'>)</mo><mo>≤</mo><mo stretchy='false'>(</mo><mi>b</mi><mo>,</mo><mi>n</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(a,m) \leq (b,n)</annotation></semantics></math> iff <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_40' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>=</mo><mi>b</mi></mrow><annotation encoding='application/x-tex'>a = b</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_41' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi><mo>≤</mo><mi>n</mi></mrow><annotation encoding='application/x-tex'>m \leq n</annotation></semantics></math> or <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_42' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>≤</mo><mi>b</mi></mrow><annotation encoding='application/x-tex'>a \leq b</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_43' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi><mo><</mo><mi>n</mi></mrow><annotation encoding='application/x-tex'>m \lt n</annotation></semantics></math>.</p> </div> <div class='num_defn' id='EventuallyAndFrequently'> <h6 id='definition_3'>Definition</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventually</a> and frequently)</strong></p> <p>Consider <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_44' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> (def. <a class='maruku-ref' href='#Net'>2</a>), and given a <a class='existingWikiWord' href='/nlab/show/diff/subset'>subset</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_45' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>⊂</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>S \subset X</annotation></semantics></math>. We say that</p> <ol> <li> <p><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_46' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> is <em><a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventually</a> in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_47' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math></em> if there exists <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_48' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>i</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>i \in A</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_49' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mi>j</mi></msub><mo>∈</mo><mi>S</mi></mrow><annotation encoding='application/x-tex'>\nu_j \in S</annotation></semantics></math> for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_50' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≥</mo><mi>i</mi></mrow><annotation encoding='application/x-tex'>j \ge i</annotation></semantics></math>.</p> </li> <li> <p><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_51' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> is <em>frequently in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_52' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math></em> if for every index <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_53' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>i</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>i \in A</annotation></semantics></math>, then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_54' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mi>j</mi></msub><mo>∈</mo><mi>S</mi></mrow><annotation encoding='application/x-tex'>\nu_j \in S</annotation></semantics></math> for some <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_55' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≥</mo><mi>i</mi></mrow><annotation encoding='application/x-tex'>j \ge i</annotation></semantics></math>.</p> </li> </ol> </div> <div class='num_remark'> <h6 id='remark_2'>Remark</h6> <p>Sometimes one says ‘infinitely often’ in place of ‘frequently’ in def. <a class='maruku-ref' href='#EventuallyAndFrequently'>3</a> and even ‘cofinitely often’ in place of ‘eventually’; these derive from the special case of sequences, where they may be taken literally.</p> </div> <div class='num_defn' id='Convergence'> <h6 id='definition_4'>Definition</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/convergence'>convergence</a> of <a class='existingWikiWord' href='/nlab/show/diff/net'>nets</a>)</strong></p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_56' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a>, and let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_57' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a> in the underlying set (def. <a class='maruku-ref' href='#Net'>2</a>).</p> <p>We say that the net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_58' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math></p> <ol> <li> <p><em><a class='existingWikiWord' href='/nlab/show/diff/convergence'>converges</a></em> to an element <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_59' 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> if given any <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhood</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_60' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_61' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_62' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> is eventually in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_63' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> (def. <a class='maruku-ref' href='#EventuallyAndFrequently'>3</a>); such <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_64' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> is called a <em><a class='existingWikiWord' href='/nlab/show/diff/limit+point'>limit point</a></em> of the net;</p> </li> <li> <p><em>clusters</em> at <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_65' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> if, for every <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhood</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_66' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_67' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_68' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> is frequently in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_69' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> (also def. <a class='maruku-ref' href='#EventuallyAndFrequently'>3</a>); such <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_70' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> is called a <em><a class='existingWikiWord' href='/nlab/show/diff/limit+point'>cluster point</a></em> of the net.</p> </li> </ol> </div> <div class='num_remark'> <h6 id='remark_3'>Remark</h6> <p>Beware that <a class='existingWikiWord' href='/nlab/show/diff/limit+point'>limit points</a> of nets, according to def. <a class='maruku-ref' href='#Convergence'>4</a>, need not be unique. They are guaranteed to be unique in <a class='existingWikiWord' href='/nlab/show/diff/Hausdorff+space'>Hausdorff spaces</a>, see prop. <a class='maruku-ref' href='#NetsDetectHausdorff'>4</a> below.</p> </div> <h3 id='subnets'>Subnets</h3> <p>The definition of the concept of <em><a class='existingWikiWord' href='/nlab/show/diff/subnet'>sub-nets</a></em> of a net requires some care. The point of the definition is to ensure that prop. <a class='maruku-ref' href='#CompactSpacesEquivalentlyHaveConvergetSubnets'>5</a> below becomes true, which states that <a class='existingWikiWord' href='/nlab/show/diff/compact+spaces+equivalently+have+converging+subnets'>compact spaces are equivalently those for which every net has a converging subnet</a>.</p> <p>There are several different definitions of ‘<a class='existingWikiWord' href='/nlab/show/diff/subnet'>subnet</a>’ in the literature, all of which intend to generalise the concept of subsequences. We state them now in order of increasing generality. Note that it is Definition <a class='maruku-ref' href='#AA'>7</a> which is correct in that it corresponds precisely to refinement of filters. However, the other two definitions (def. <a class='maruku-ref' href='#Willard'>5</a>, def. <a class='maruku-ref' href='#Kelley'>6</a>) are sufficient (in a sense made precise by theorem <a class='maruku-ref' href='#EquivalenceOfDefinitionsOfSubnets'>1</a> below) and may be easier to work with.</p> <div class='num_defn' id='Willard'> <h6 id='definition_5'>Definition</h6> <p>(Willard, 1970).</p> <p>Given a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_71' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>x</mi> <mi>α</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(x_{\alpha})</annotation></semantics></math> with index set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_72' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math>, and a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_73' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>y</mi> <mi>β</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(y_{\beta})</annotation></semantics></math> with an index set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_74' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math>, we say that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_75' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> is a <strong>subnet</strong> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_76' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> if:</p> <p>We have a <a class='existingWikiWord' href='/nlab/show/diff/function'>function</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_77' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>f\colon B \to A</annotation></semantics></math> such that</p> <ul> <li><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_78' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> maps <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_79' 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_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_80' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> (that is, for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_81' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>\beta \in B</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_82' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>y</mi> <mi>β</mi></msub><mo>=</mo><msub><mi>x</mi> <mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>β</mi><mo stretchy='false'>)</mo></mrow></msub></mrow><annotation encoding='application/x-tex'>y_{\beta} = x_{f(\beta)}</annotation></semantics></math>);</li> <li><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_83' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> is monotone (that is, for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_84' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>β</mi> <mn>1</mn></msub><mo>≥</mo><msub><mi>β</mi> <mn>2</mn></msub><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>\beta_1 \geq \beta_2 \in B</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_85' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>β</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo><mo>≥</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>β</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f(\beta_1) \geq f(\beta_2)</annotation></semantics></math>);</li> <li><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_86' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> is cofinal (that is, for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_87' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>α</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>\alpha \in A</annotation></semantics></math> there is a <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_88' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>\beta \in B</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_89' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>β</mi><mo stretchy='false'>)</mo><mo>≥</mo><mi>α</mi></mrow><annotation encoding='application/x-tex'>f(\beta) \geq \alpha</annotation></semantics></math>).</li> </ul> </div> <div class='num_defn' id='Kelley'> <h6 id='definition_6'>Definition</h6> <p>(Kelley, 1955).</p> <p>Given a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_90' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>x</mi> <mi>α</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(x_{\alpha})</annotation></semantics></math> with index set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_91' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math>, and a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_92' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>y</mi> <mi>β</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(y_{\beta})</annotation></semantics></math> with an index set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_93' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math>, we say that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_94' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> is a <strong>subnet</strong> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_95' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> if:</p> <p>We have a <a class='existingWikiWord' href='/nlab/show/diff/function'>function</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_96' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>f\colon B \to A</annotation></semantics></math> such that</p> <ul> <li><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_97' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> maps <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_98' 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_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_99' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> (that is, for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_100' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>\beta \in B</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_101' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>y</mi> <mi>β</mi></msub><mo>=</mo><msub><mi>x</mi> <mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>β</mi><mo stretchy='false'>)</mo></mrow></msub></mrow><annotation encoding='application/x-tex'>y_{\beta} = x_{f(\beta)}</annotation></semantics></math>);</li> <li><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_102' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> is strongly cofinal (that is, for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_103' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>α</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>\alpha \in A</annotation></semantics></math> there is a <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_104' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>\beta \in B</annotation></semantics></math> such that, for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_105' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>β</mi> <mn>1</mn></msub><mo>≥</mo><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>\beta_1 \geq \beta \in B</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_106' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>β</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo><mo>≥</mo><mi>α</mi></mrow><annotation encoding='application/x-tex'>f(\beta_1) \geq \alpha</annotation></semantics></math>).</li> </ul> </div> <div class='num_remark'> <h6 id='remark_4'>Remark</h6> <p>Notice that the function <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_107' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> in definitions <a class='maruku-ref' href='#Willard'>5</a> and <a class='maruku-ref' href='#Kelley'>6</a> is <em>not</em> required to be an <a class='existingWikiWord' href='/nlab/show/diff/injection'>injection</a>, and it need not be. As a result, a <a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequence</a> regarded as a <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a> in general has more sub-nets than it has sub-sequences.</p> </div> <div class='num_defn' id='AA'> <h6 id='definition_7'>Definition</h6> <p>(Smiley, 1957; Årnes & Andenæs, 1972).</p> <p>Given a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_108' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>x</mi> <mi>α</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(x_{\alpha})</annotation></semantics></math> with index set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_109' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math>, and a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_110' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>y</mi> <mi>β</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(y_{\beta})</annotation></semantics></math> with an index set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_111' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math>, we say that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_112' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> is a <strong>subnet</strong> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_113' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> if:</p> <p>The <a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filter</a> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_114' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> (def. <a class='maruku-ref' href='#EventualityFilter'>9</a>) refines the eventuality filter of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_115' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>. (Explicitly, for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_116' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>α</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>\alpha \in A</annotation></semantics></math> there is a <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_117' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>\beta \in B</annotation></semantics></math> such that, for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_118' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>β</mi> <mn>1</mn></msub><mo>≥</mo><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>\beta_1 \geq \beta \in B</annotation></semantics></math> there is an <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_119' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>α</mi> <mn>1</mn></msub><mo>≥</mo><mi>α</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>\alpha_1 \geq \alpha \in A</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_120' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>y</mi> <mrow><msub><mi>β</mi> <mn>1</mn></msub></mrow></msub><mo>=</mo><msub><mi>x</mi> <mrow><msub><mi>α</mi> <mn>1</mn></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>y_{\beta_1} = x_{\alpha_1}</annotation></semantics></math>.)</p> </div> <p>The equivalence between these definitions is as follows:</p> <div class='num_theorem' id='EquivalenceOfDefinitionsOfSubnets'> <h6 id='theorem'>Theorem</h6> <p>(<a href='#Schechter96'>Schechter, 1996</a>).</p> <ol> <li>If <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_121' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> is a (<a class='maruku-ref' href='#Willard'>5</a>)-subnet of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_122' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_123' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> is also a (<a class='maruku-ref' href='#Kelley'>6</a>)-subnet of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_124' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, using the same function <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_125' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math>.</li> <li>If <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_126' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> is a (<a class='maruku-ref' href='#Kelley'>6</a>)-subnet of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_127' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_128' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> is also a (<a class='maruku-ref' href='#AA'>7</a>)-subnet of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_129' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>.</li> <li>If <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_130' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> is a (<a class='maruku-ref' href='#AA'>7</a>)-subnet of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_131' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, then there is some net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_132' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>z</mi></mrow><annotation encoding='application/x-tex'>z</annotation></semantics></math> such that <ul> <li><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_133' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>z</mi></mrow><annotation encoding='application/x-tex'>z</annotation></semantics></math> is equivalent to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_134' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> in the sense that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_135' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi></mrow><annotation encoding='application/x-tex'>y</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_136' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>z</mi></mrow><annotation encoding='application/x-tex'>z</annotation></semantics></math> are (<a class='maruku-ref' href='#AA'>7</a>)-subnets of each other, and</li> <li><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_137' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>z</mi></mrow><annotation encoding='application/x-tex'>z</annotation></semantics></math> is a (<a class='maruku-ref' href='#Willard'>5</a>)-subnet of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_138' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, using some function.</li> </ul> </li> </ol> </div> <p>So from the perspective of definition (<a class='maruku-ref' href='#AA'>7</a>), there are enough (<a class='maruku-ref' href='#Willard'>5</a>)-subnets and (<a class='maruku-ref' href='#Kelley'>6</a>)-subnets, up to equivalence.</p> <h3 id='NetsAndFilters'>Eventuality filters</h3> <p>Recall that:</p> <div class='num_defn' id='Filter'> <h6 id='definition_8'>Definition</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/filter'>filter</a>)</strong></p> <p>Given a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_139' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> then a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> of <a class='existingWikiWord' href='/nlab/show/diff/subset'>subsets</a> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_140' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>, hence a subset of the <a class='existingWikiWord' href='/nlab/show/diff/power+set'>power set</a></p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_141' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℱ</mi><mo>⊂</mo><mi>P</mi><mo stretchy='false'>(</mo><mi>X</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'> \mathcal{F} \subset P(X) </annotation></semantics></math></div> <p>is called a <em><a class='existingWikiWord' href='/nlab/show/diff/filter'>filter</a></em> of subsets if it is closed under <a class='existingWikiWord' href='/nlab/show/diff/intersection'>intersections</a> and under taking supersets.</p> <p>The filter <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_142' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℱ</mi></mrow><annotation encoding='application/x-tex'>\mathcal{F}</annotation></semantics></math> is called <em>proper</em> if each set in it is <a class='existingWikiWord' href='/nlab/show/diff/inhabited+set'>inhabited</a>.</p> </div> <div class='num_defn' id='EventualityFilter'> <h6 id='definition_9'>Definition</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filter</a>)</strong></p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_143' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> and let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_144' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>D</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon D \to X</annotation></semantics></math> be a net in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_145' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> (def. <a class='maruku-ref' href='#Net'>2</a>).</p> <p>The <em><a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filter</a></em> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_146' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ℱ</mi> <mi>ν</mi></msub></mrow><annotation encoding='application/x-tex'>\mathcal{F}_\nu</annotation></semantics></math> of the net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_147' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> is the <a class='existingWikiWord' href='/nlab/show/diff/filter'>filter</a> (def. <a class='maruku-ref' href='#Filter'>8</a>) onsisting of the subsets that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_148' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> is <em>eventually in</em>, according to def. <a class='maruku-ref' href='#EventuallyAndFrequently'>3</a>.</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_149' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mo>(</mo><mo stretchy='false'>(</mo><mi>U</mi><mo>⊂</mo><mi>X</mi><mo stretchy='false'>)</mo><mo>∈</mo><msub><mi>ℱ</mi> <mi>ν</mi></msub><mo>)</mo></mrow><mspace width='thinmathspace' /><mo>⇔</mo><mspace width='thinmathspace' /><mrow><mo>(</mo><mi>ν</mi><mspace width='thinmathspace' /><mtext>is eventually in</mtext><mspace width='thinmathspace' /><mi>U</mi><mo>)</mo></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> \left( (U \subset X) \in \mathcal{F}_\nu \right) \,\Leftrightarrow\, \left( \nu \, \text{is eventually in}\, U \right) \,. </annotation></semantics></math></div></div> <div class='num_remark'> <h6 id='remark_5'>Remark</h6> <p><strong>(equivalence of nets)</strong></p> <p>Two nets are to be considered <strong>equivalent</strong> if they have the same <a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filter</a> according to def. <a class='maruku-ref' href='#EventualityFilter'>9</a>. By def. <a class='maruku-ref' href='#AA'>7</a> and theorem <a class='maruku-ref' href='#EquivalenceOfDefinitionsOfSubnets'>1</a>, this means equivalently that they are both subnets of each other.</p> <p>In particular, equivalent nets define the same logical quantifiers (see <a href='#LogicOfNets'>below</a>) and are therefore indeed equivalent for the application to <a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a> (see <a href='#RelationToTopology'>below</a>).</p> <p>(Of course, it is possible to distinguish them by using the standard logical quantifiers instead.)</p> </div> <p>Conversely, every <a class='existingWikiWord' href='/nlab/show/diff/filter'>filter</a> is the <a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filter</a> of some net:</p> <div class='num_defn' id='FilterNet'> <h6 id='definition_10'>Definition</h6> <p><strong>(nets from filters)</strong></p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_150' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> and let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_151' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℱ</mi><mo>⊂</mo><mi>P</mi><mo stretchy='false'>(</mo><mi>X</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\mathcal{F} \subset P(X)</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/filter'>filter</a> of subsets of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_152' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> (def. <a class='maruku-ref' href='#Filter'>8</a>). Ss Consider the <a class='existingWikiWord' href='/nlab/show/diff/disjoint+union'>disjoint union</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_153' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><munder><mo>⊔</mo><mrow><mi>U</mi><mo>∈</mo><mi>ℱ</mi></mrow></munder></mrow><annotation encoding='application/x-tex'>\underset{U \in \mathcal{F}}{\sqcup}</annotation></semantics></math> of subsets in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_154' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℱ</mi></mrow><annotation encoding='application/x-tex'>\mathcal{F}</annotation></semantics></math>, hence the set whose elements are <a class='existingWikiWord' href='/nlab/show/diff/pair'>pairs</a> of the form <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_155' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>U</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(U,x)</annotation></semantics></math>, where <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_156' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><mi>U</mi><mo>∈</mo><mi>ℱ</mi></mrow><annotation encoding='application/x-tex'>x \in U \in \mathcal{F}</annotation></semantics></math>. Equipped with the ordering</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_157' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mo>(</mo><mo stretchy='false'>(</mo><mi>U</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>≥</mo><mo stretchy='false'>(</mo><mi>V</mi><mo>,</mo><mi>y</mi><mo stretchy='false'>)</mo><mo>)</mo></mrow><mspace width='thinmathspace' /><mo>⇔</mo><mspace width='thinmathspace' /><mrow><mo>(</mo><mi>U</mi><mo>⊂</mo><mi>V</mi><mo>)</mo></mrow><mphantom><mi>AAA</mi></mphantom><mtext>regardless of</mtext><mspace width='thinmathspace' /><mi>x</mi><mspace width='thinmathspace' /><mtext>and</mtext><mspace width='thinmathspace' /><mi>y</mi></mrow><annotation encoding='application/x-tex'> \left( (U,x) \geq (V,y) \right) \,\Leftrightarrow\, \left( U \subset V \right) \phantom{AAA} \text{regardless of}\, x\, \text{and} \, y </annotation></semantics></math></div> <p>the fact that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_158' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℱ</mi></mrow><annotation encoding='application/x-tex'>\mathcal{F}</annotation></semantics></math> is a proper filter implies that this is a <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a> according to def. <a class='maruku-ref' href='#DirectedSet'>1</a>. (It is actually enough to use only a base of the filters).</p> <p>Then the <em>filter net</em> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_159' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mi>F</mi></msub></mrow><annotation encoding='application/x-tex'>\nu_F</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_160' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℱ</mi></mrow><annotation encoding='application/x-tex'>\mathcal{F}</annotation></semantics></math> is the <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a> on <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_161' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> (def. <a class='maruku-ref' href='#Net'>2</a>) given by</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_162' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable><mtr><mtd><msub><mrow><mo>(</mo><munder><mo>⊔</mo><mrow><mi>U</mi><mo>∈</mo><mi>ℱ</mi></mrow></munder><mi>U</mi><mo>)</mo></mrow> <mo>⊃</mo></msub></mtd> <mtd><mover><mo>⟶</mo><mrow><msub><mi>ν</mi> <mi>ℱ</mi></msub></mrow></mover></mtd> <mtd><mi>X</mi></mtd></mtr> <mtr><mtd><mo stretchy='false'>(</mo><mi>U</mi><mo>,</mo><mi>x</mi><mo stretchy='false'>)</mo></mtd> <mtd><mover><mo>↦</mo><mphantom><mi>AAA</mi></mphantom></mover></mtd> <mtd><mi>x</mi></mtd></mtr></mtable></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> \array{ \left( \underset{U \in \mathcal{F}}{\sqcup} U \right)_{\supset} &\overset{\nu_{\mathcal{F}}}{\longrightarrow}& X \\ (U,x) &\overset{\phantom{AAA}}{\mapsto}& x } \,. </annotation></semantics></math></div></div> <div class='num_prop'> <h6 id='proposition'>Proposition</h6> <p>Given a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_163' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> and a <a class='existingWikiWord' href='/nlab/show/diff/filter'>filter</a> of subsets <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_164' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℱ</mi><mo>⊂</mo><mi>P</mi><mo stretchy='false'>(</mo><mi>X</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\mathcal{F} \subset P(X)</annotation></semantics></math> (def. <a class='maruku-ref' href='#Filter'>8</a>), then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_165' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℱ</mi></mrow><annotation encoding='application/x-tex'>\mathcal{F}</annotation></semantics></math> is the <a class='existingWikiWord' href='/nlab/show/diff/eventuality+filter'>eventuality filter</a> (def. <a class='maruku-ref' href='#EventualityFilter'>9</a>) of its filter net (def. <a class='maruku-ref' href='#FilterNet'>10</a>).</p> </div> <h2 id='properties'>Properties</h2> <h3 id='RelationToTopology'>Relation to topology</h3> <p>We discuss that nets detect:</p> <ol> <li> <p>the topology on general topological spaces (prop. <a class='maruku-ref' href='#TopologyDetectedByNets'>2</a> below),</p> </li> <li> <p>the continuity of functions between them (prop. <a class='maruku-ref' href='#ContinuousFunctionsDetectedByNets'>3</a> below),</p> </li> <li> <p>the <a class='existingWikiWord' href='/nlab/show/diff/Hausdorff+space'>Hausdorff</a> property (prop. <a class='maruku-ref' href='#NetsDetectHausdorff'>4</a> below),</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compactness</a> (prop. <a class='maruku-ref' href='#CompactSpacesEquivalentlyHaveConvergetSubnets'>5</a> below).</p> </li> </ol> <div class='num_prop' id='TopologyDetectedByNets'> <h6 id='proposition_2'>Proposition</h6> <p><strong>(topology detected by nets)</strong></p> <p>Using the <a class='existingWikiWord' href='/nlab/show/diff/axiom+of+choice'>axiom of choice</a> then:</p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_166' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X, \tau)</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a>. Then a <a class='existingWikiWord' href='/nlab/show/diff/subset'>subset</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_167' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>S</mi><mo>⊂</mo><mi>X</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(S \subset X)</annotation></semantics></math> is <a class='existingWikiWord' href='/nlab/show/diff/open+subspace'>open</a> in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_168' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> (is an element of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_169' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>τ</mi><mo>⊂</mo><mi>P</mi><mo stretchy='false'>(</mo><mi>X</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\tau \subset P(X)</annotation></semantics></math>) precisely if its <a class='existingWikiWord' href='/nlab/show/diff/complement'>complement</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_170' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi><mo>\</mo><mi>S</mi></mrow><annotation encoding='application/x-tex'>X \backslash S</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/closed+subspace'>closed subset</a> as seen not just by sequences but by nets, in that no <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a> with elements in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_171' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi><mo>\</mo><mi>S</mi></mrow><annotation encoding='application/x-tex'>X\backslash S</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_172' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi><mo>\</mo><mi>S</mi><mo>↪</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X\backslash S \hookrightarrow X</annotation></semantics></math>, <a class='existingWikiWord' href='/nlab/show/diff/convergence'>converges</a> to an element in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_173' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>.</p> </div> <div class='proof'> <h6 id='proof'>Proof</h6> <p>In one direction, let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_174' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>⊂</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>S \subset X</annotation></semantics></math> be open, and consider a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_175' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi><mo>\</mo><mi>S</mi><mo>⊂</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X \backslash S \subset X</annotation></semantics></math>. We need to show that for every point <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_176' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding='application/x-tex'>x \in S</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_177' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> is not a limiting point of the net.</p> <p>But by assumption then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_178' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhood</a> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_179' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> which does not contain any element of the net, and so by definition of convergence it is not a limit of this net.</p> <p>Conversely, let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_180' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>⊂</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>S \subset X</annotation></semantics></math> be a subset that is not open. We need to show that then there exists a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_181' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi><mo>\</mo><mi>S</mi><mo>⊂</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X\backslash S \subset X</annotation></semantics></math> that converges to a point in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_182' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>.</p> <p>For <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_183' 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>, consider the <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_184' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><mi>x</mi><msub><mo stretchy='false'>)</mo> <mo>⊃</mo></msub></mrow><annotation encoding='application/x-tex'>Nbhd_X(x)_{\supset}</annotation></semantics></math> of <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>open neighbourhoods</a> of this element (example <a class='maruku-ref' href='#DirectedSetOfNeighbourhods'>2</a>). Now the fact that the set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_185' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is not open means that there exists an element <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_186' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>s</mi><mo>∈</mo><mi>S</mi><mo>⊂</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>s \in S \subset X</annotation></semantics></math> such that every <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>open neighbourhood</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_187' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_188' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>s</mi></mrow><annotation encoding='application/x-tex'>s</annotation></semantics></math> intersects <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_189' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi><mo>\</mo><mi>S</mi></mrow><annotation encoding='application/x-tex'>X \backslash S</annotation></semantics></math>. This means that we may <a class='existingWikiWord' href='/nlab/show/diff/axiom+of+choice'>choose</a> elements <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_190' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mi>U</mi></msub><mo>∈</mo><mi>U</mi><mo>∩</mo><mo stretchy='false'>(</mo><mi>X</mi><mo>\</mo><mi>S</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>x_U \in U \cap (X \backslash S)</annotation></semantics></math>, and hence define a net</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_191' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable><mtr><mtd><msub><mi>Nbhds</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><mi>s</mi><mo stretchy='false'>)</mo></mtd> <mtd><mover><mo>⟶</mo><mi>ν</mi></mover></mtd> <mtd><mi>X</mi><mo>\</mo><mi>S</mi><mo>⊂</mo><mi>X</mi></mtd></mtr> <mtr><mtd><mi>U</mi></mtd> <mtd><mo>↦</mo></mtd> <mtd><msub><mi>x</mi> <mi>U</mi></msub></mtd></mtr></mtable></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> \array{ Nbhds_X(s) &\overset{\nu}{\longrightarrow}& X \backslash S \subset X \\ U &\mapsto& x_U } \,. </annotation></semantics></math></div> <p>But by construction this net has the property that for every neighbourhood <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_192' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>V</mi></mrow><annotation encoding='application/x-tex'>V</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_193' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>s</mi></mrow><annotation encoding='application/x-tex'>s</annotation></semantics></math> there exists <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_194' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi><mo>∈</mo><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><mi>s</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>U \in Nbhd_X(s)</annotation></semantics></math> such that for all <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_195' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi><mo>′</mo><mo>⊂</mo><mi>U</mi></mrow><annotation encoding='application/x-tex'>U' \subset U</annotation></semantics></math> then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_196' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mrow><mi>U</mi><mo>′</mo></mrow></msub><mo>∈</mo><mi>V</mi></mrow><annotation encoding='application/x-tex'>x_{U'} \in V</annotation></semantics></math>, namely <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_197' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi><mo>=</mo><mi>V</mi></mrow><annotation encoding='application/x-tex'>U = V</annotation></semantics></math>. Hence the net converges to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_198' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>s</mi></mrow><annotation encoding='application/x-tex'>s</annotation></semantics></math>.</p> </div> <div class='num_prop' id='ContinuousFunctionsDetectedByNets'> <h6 id='proposition_3'>Proposition</h6> <p><strong>(continuous functions detected by nets)</strong></p> <p><span><del class='diffmod'> Assuming</del><ins class='diffmod'> Let</ins></span><del class='diffmod'><a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a></del><ins class='diffmod'><math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_199' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><msub><mi>τ</mi> <mi>X</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau_X)</annotation></semantics></math></ins><span><del class='diffmod'> ,</del><ins class='diffmod'> </ins><del class='diffmod'> then</del><ins class='diffmod'> and</ins></span><ins class='diffins'><math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_200' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>Y</mi><mo>,</mo><msub><mi>τ</mi> <mi>Y</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(Y,\tau_Y)</annotation></semantics></math></ins><ins class='diffins'> be two </ins><ins class='diffins'><a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a></ins><ins class='diffins'>. Then a </ins><ins class='diffins'><a class='existingWikiWord' href='/nlab/show/diff/function'>function</a></ins><ins class='diffins'> </ins><ins class='diffins'><math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_201' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>f \colon X \to Y</annotation></semantics></math></ins><ins class='diffins'> between their underlying sets is </ins><ins class='diffins'><a class='existingWikiWord' href='/nlab/show/diff/continuous+map'>continuous</a></ins><ins class='diffins'> precisely if for every net </ins><ins class='diffins'><math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_202' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math></ins><ins class='diffins'> that </ins><ins class='diffins'><a class='existingWikiWord' href='/nlab/show/diff/convergence'>converges</a></ins><ins class='diffins'> to some </ins><ins class='diffins'><a class='existingWikiWord' href='/nlab/show/diff/limit+point'>limit point</a></ins><ins class='diffins'> </ins><ins class='diffins'><math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_203' 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></ins><ins class='diffins'> (def. </ins><ins class='diffins'><a class='maruku-ref' href='#Convergence'>4</a></ins><ins class='diffins'>), the image net </ins><ins class='diffins'><math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_204' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f\circ \nu</annotation></semantics></math></ins><ins class='diffins'> converges to </ins><ins class='diffins'><math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_205' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>∈</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>f(x)\in Y</annotation></semantics></math></ins><ins class='diffins'>.</ins></p><del class='diffdel'> </del><del class='diffdel'><p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_199' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><msub><mi>τ</mi> <mi>X</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau_X)</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_200' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>Y</mi><mo>,</mo><msub><mi>τ</mi> <mi>Y</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(Y,\tau_Y)</annotation></semantics></math> be two <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a>. Then a <a class='existingWikiWord' href='/nlab/show/diff/function'>function</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_201' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>f \colon X \to Y</annotation></semantics></math> between their underlying sets is <a class='existingWikiWord' href='/nlab/show/diff/continuous+map'>continuous</a> precisely if for every net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_202' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> that <a class='existingWikiWord' href='/nlab/show/diff/convergence'>converges</a> to some <a class='existingWikiWord' href='/nlab/show/diff/limit+point'>limit point</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_203' 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> (def. <a class='maruku-ref' href='#Convergence'>4</a>), the image net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_204' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f\circ \nu</annotation></semantics></math> converges to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_205' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>∈</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>f(x)\in Y</annotation></semantics></math>.</p></del> </div> <div class='proof'> <h6 id='proof_2'>Proof</h6> <p>In one direction, suppose that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_206' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>f \colon X \to Y</annotation></semantics></math> is continuous, and that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_207' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> converges to some <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_208' 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>. We need to show that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_209' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f \circ \nu</annotation></semantics></math> converges to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_210' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>∈</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>f(x) \in Y</annotation></semantics></math>, hence that for every neighbourhood <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_211' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow></msub><mo>⊂</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>U_{f(x)} \subset Y</annotation></semantics></math> there exists <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_212' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>i</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>i \in A</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_213' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>ν</mi><mo stretchy='false'>(</mo><mi>j</mi><mo stretchy='false'>)</mo><mo stretchy='false'>)</mo><mo>∈</mo><msub><mi>U</mi> <mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow></msub></mrow><annotation encoding='application/x-tex'>f(\nu(j)) \in U_{f(x)}</annotation></semantics></math> for all <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_214' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≥</mo><mi>i</mi></mrow><annotation encoding='application/x-tex'>j \geq i</annotation></semantics></math>.</p> <p>But since <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_215' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> is continuous, the <a class='existingWikiWord' href='/nlab/show/diff/preimage'>pre-image</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_216' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><msub><mi>U</mi> <mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow></msub><mo stretchy='false'>)</mo><mo>⊂</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>f^{-1}(U_{f(x)}) \subset X</annotation></semantics></math> is an open neighbourhood of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_217' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, and so by the assumption that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_218' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> converges there is an <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_219' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>i</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>i \in A</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_220' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo stretchy='false'>(</mo><mi>j</mi><mo stretchy='false'>)</mo><mo>∈</mo><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><msub><mi>U</mi> <mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\nu(j) \in f^{-1}(U_{f(x)})</annotation></semantics></math> for all <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_221' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≥</mo><mi>i</mi></mrow><annotation encoding='application/x-tex'>j \geq i</annotation></semantics></math>. By applying <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_222' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math>, this is the required statement.</p> <p>We give two proofs of the other direction.</p> <p><em>proof 1</em></p> <p><span><del class='diffmod'> Conversely,</del><ins class='diffmod'> Assuming</ins><del class='diffdel'> suppose</del><del class='diffdel'> that</del></span><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_223' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math></del><del class='diffdel'> is not continuous. We need to find a net </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_224' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math></del><del class='diffdel'> that converges to some </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_225' 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></del><del class='diffdel'>, and show that </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_226' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f \circ \nu</annotation></semantics></math></del><del class='diffdel'> does not converge to </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_227' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f(x)</annotation></semantics></math></del><del class='diffdel'>. (This is the </del><del class='diffdel'><a class='existingWikiWord' href='/nlab/show/diff/contrapositive'>contrapositive</a></del><del class='diffdel'> of the reverse implication, and by </del><a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a><span><del class='diffmod'> </del><ins class='diffmod'> ,</ins><del class='diffdel'> equivalent</del><del class='diffdel'> to</del><del class='diffdel'> it.)</del></span></p> <p><span><del class='diffmod'> Now</del><ins class='diffmod'> Conversely,</ins><ins class='diffins'> suppose</ins> that</span><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_228' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math><span> is not<del class='diffmod'> continuous</del><ins class='diffmod'> continuous.</ins><del class='diffmod'> means</del><ins class='diffmod'> We</ins><del class='diffmod'> that</del><ins class='diffmod'> need</ins><del class='diffmod'> there</del><ins class='diffmod'> to</ins><del class='diffmod'> exists</del><ins class='diffmod'> find</ins><del class='diffmod'> an</del><ins class='diffmod'> a</ins><del class='diffmod'> open</del><ins class='diffmod'> net</ins><del class='diffdel'> subset</del></span><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_229' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi><span><del class='diffmod'> U</del><ins class='diffmod'> ν</ins></span></mi><del class='diffdel'><mo>⊂</mo></del><del class='diffdel'><mi>Y</mi></del></mrow><annotation encoding='application/x-tex'><span><del class='diffmod'> U</del><ins class='diffmod'> \nu</ins><del class='diffdel'> \subset</del><del class='diffdel'> Y</del></span></annotation></semantics></math><span> <del class='diffdel'> such</del> that<del class='diffmod'> the</del><ins class='diffmod'> converges</ins><del class='diffmod'> pre-image</del><ins class='diffmod'> to</ins><ins class='diffins'> some</ins></span><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_230' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><del class='diffmod'><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup></del><ins class='diffmod'><mi>x</mi></ins><mo stretchy='false'><span><del class='diffmod'> (</del><ins class='diffmod'> ∈</ins></span></mo><mi><span><del class='diffmod'> U</del><ins class='diffmod'> X</ins></span></mi><del class='diffdel'><mo stretchy='false'>)</mo></del></mrow><annotation encoding='application/x-tex'><span><del class='diffmod'> f^{-1}(U)</del><ins class='diffmod'> x</ins><ins class='diffins'> \in</ins><ins class='diffins'> X</ins></span></annotation></semantics></math><span><del class='diffmod'> </del><ins class='diffmod'> ,</ins><del class='diffmod'> is</del><ins class='diffmod'> and</ins><del class='diffmod'> not</del><ins class='diffmod'> show</ins><del class='diffmod'> open.</del><ins class='diffmod'> that</ins><del class='diffdel'> By</del><del class='diffdel'> prop.</del></span><del class='diffmod'><a class='maruku-ref' href='#TopologyDetectedByNets'>2</a></del><ins class='diffmod'><math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_226' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f \circ \nu</annotation></semantics></math></ins><span> <del class='diffmod'> this</del><ins class='diffmod'> does</ins><del class='diffmod'> means</del><ins class='diffmod'> not</ins><del class='diffmod'> that</del><ins class='diffmod'> converge</ins><del class='diffmod'> there</del><ins class='diffmod'> to</ins><del class='diffdel'> exists</del><del class='diffdel'> a</del><del class='diffdel'> net</del></span><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_231' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi><span><del class='diffmod'> ν</del><ins class='diffmod'> f</ins></span></mi><ins class='diffins'><mo stretchy='false'>(</mo></ins><ins class='diffins'><mi>x</mi></ins><ins class='diffins'><mo stretchy='false'>)</mo></ins></mrow><annotation encoding='application/x-tex'><span><del class='diffmod'> \nu</del><ins class='diffmod'> f(x)</ins></span></annotation></semantics></math><span><del class='diffmod'> </del><ins class='diffmod'> .</ins><del class='diffmod'> in</del><ins class='diffmod'> (This</ins><ins class='diffins'> is</ins><ins class='diffins'> the</ins></span><del class='diffmod'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_232' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi><mo>\</mo><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>U</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>X \backslash f^{-1}(U)</annotation></semantics></math></del><ins class='diffmod'><a class='existingWikiWord' href='/nlab/show/diff/contrapositive'>contrapositive</a></ins><span> <del class='diffmod'> that</del><ins class='diffmod'> of</ins><del class='diffmod'> converges</del><ins class='diffmod'> the</ins><del class='diffmod'> to</del><ins class='diffmod'> reverse</ins><del class='diffmod'> an</del><ins class='diffmod'> implication,</ins><del class='diffmod'> element</del><ins class='diffmod'> and</ins><ins class='diffins'> by</ins></span><del class='diffmod'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_233' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>U</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>x \in f^{-1}(U)</annotation></semantics></math></del><ins class='diffmod'><a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a></ins><span><del class='diffmod'> .</del><ins class='diffmod'> </ins><del class='diffmod'> But</del><ins class='diffmod'> equivalent</ins><del class='diffmod'> this</del><ins class='diffmod'> to</ins><del class='diffmod'> means</del><ins class='diffmod'> it.)</ins><del class='diffdel'> that</del></span><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_234' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f \circ \nu</annotation></semantics></math></del><del class='diffdel'> is a net in the </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_235' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Y</mi><mo>\</mo><mi>U</mi></mrow><annotation encoding='application/x-tex'>Y \backslash U</annotation></semantics></math></del><del class='diffdel'>, which is a </del><del class='diffdel'><a class='existingWikiWord' href='/nlab/show/diff/closed+subspace'>closed subset</a></del><del class='diffdel'> by the assumption that </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_236' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math></del><del class='diffdel'> is open. Again by prop. </del><del class='diffdel'><a class='maruku-ref' href='#TopologyDetectedByNets'>2</a></del><del class='diffdel'> this means that </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_237' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f\circ \nu</annotation></semantics></math></del><del class='diffdel'> converges to an element in </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_238' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Y</mi><mo>\</mo><mi>U</mi></mrow><annotation encoding='application/x-tex'>Y \backslash U</annotation></semantics></math></del><del class='diffdel'>, and hence not to </del><del class='diffdel'><math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_239' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>∈</mo><mi>U</mi></mrow><annotation encoding='application/x-tex'>f(x) \in U</annotation></semantics></math></del><del class='diffdel'>.</del></p> <ins class='diffins'><p>Now that <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_228' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> is not continuous means that there exists an open subset <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_229' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi><mo>⊂</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>U \subset Y</annotation></semantics></math> such that the pre-image <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_230' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>U</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f^{-1}(U)</annotation></semantics></math> is not open. By prop. <a class='maruku-ref' href='#TopologyDetectedByNets'>2</a> this means that there exists a net <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_231' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> in <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_232' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi><mo>\</mo><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>U</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>X \backslash f^{-1}(U)</annotation></semantics></math> that converges to an element <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_233' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>U</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>x \in f^{-1}(U)</annotation></semantics></math>. But this means that <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_234' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f \circ \nu</annotation></semantics></math> is a net in the <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_235' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Y</mi><mo>\</mo><mi>U</mi></mrow><annotation encoding='application/x-tex'>Y \backslash U</annotation></semantics></math>, which is a <a class='existingWikiWord' href='/nlab/show/diff/closed+subspace'>closed subset</a> by the assumption that <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_236' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi></mrow><annotation encoding='application/x-tex'>U</annotation></semantics></math> is open. Again by prop. <a class='maruku-ref' href='#TopologyDetectedByNets'>2</a> this means that <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_237' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f\circ \nu</annotation></semantics></math> converges to an element in <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_238' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Y</mi><mo>\</mo><mi>U</mi></mrow><annotation encoding='application/x-tex'>Y \backslash U</annotation></semantics></math>, and hence not to <math class='maruku-mathml' display='inline' id='mathml_69564d7eb82629727315e32b5fdd80ac36e00f9d_239' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>∈</mo><mi>U</mi></mrow><annotation encoding='application/x-tex'>f(x) \in U</annotation></semantics></math>.</p></ins><ins class='diffins'> </ins><p><em>proof 2 (not using excluded middle)</em></p> <p>Assume for every net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_240' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> that converges to some limit point <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_241' 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 image net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_242' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f\circ \nu</annotation></semantics></math> converges to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_243' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>∈</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>f(x)\in Y</annotation></semantics></math>. It is sufficient to prove that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_244' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> is continuous.</p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_245' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>V</mi><mo>⊂</mo><mi>Y</mi></mrow><annotation encoding='application/x-tex'>V \subset Y</annotation></semantics></math> be open. It is sufficient to prove that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_246' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>V</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f^{-1}(V)</annotation></semantics></math> is open.</p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_247' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> be a net with range contained in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_248' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi><mo>\</mo><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>V</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>X \backslash f^{-1}(V)</annotation></semantics></math>. Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_249' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> be a limit point of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_250' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math>. By <a class='maruku-ref' href='#TopologyDetectedByNets'>2</a>, it is sufficient to prove that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_251' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∉</mo><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>V</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>x\notin f^{-1}(V)</annotation></semantics></math>.</p> <p>By our assumption, and since <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_252' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> converges to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_253' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_254' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding='application/x-tex'>f \circ \nu</annotation></semantics></math> converges to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_255' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f(x)</annotation></semantics></math>. So by <a class='maruku-ref' href='#TopologyDetectedByNets'>2</a>, since <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_256' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>V</mi></mrow><annotation encoding='application/x-tex'>V</annotation></semantics></math> is open, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_257' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>∉</mo><mi>V</mi></mrow><annotation encoding='application/x-tex'>f(x) \notin V</annotation></semantics></math>. So <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_258' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∉</mo><msup><mi>f</mi> <mrow><mo lspace='verythinmathspace' rspace='0em'>−</mo><mn>1</mn></mrow></msup><mo stretchy='false'>(</mo><mi>V</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>x \notin f^{-1}(V)</annotation></semantics></math>.</p> </div> <div class='num_remark'> <h6 id='remark_6'>Remark</h6> <p>It is possible to define elementary conditions on this <a class='existingWikiWord' href='/nlab/show/diff/convergence'>convergence</a> relation that characterise whether it is topological (that is whether it comes from a topology on <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_259' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>), although these are a bit complicated.</p> <p>By keeping only the simple conditions, one gets the definition of a <a class='existingWikiWord' href='/nlab/show/diff/convergence+space'>convergence space</a>; this is a more general concept than a topological space and includes many non-topological situations where we want to say that a sequence converges to some value (such as convergence in measure).</p> </div> <div class='num_prop' id='NetsDetectHausdorff'> <h6 id='proposition_4'>Proposition</h6> <p><strong>(Hausdorff property detected by nets)</strong></p> <p>Assuming <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a> and the <a class='existingWikiWord' href='/nlab/show/diff/axiom+of+choice'>axiom of choice</a>, then:</p> <p>A <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_260' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> is <a class='existingWikiWord' href='/nlab/show/diff/Hausdorff+space'>Hausdorff topological space</a> precisely if no <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a> in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_261' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> (def. <a class='maruku-ref' href='#Net'>2</a>) converges to two distinct <a class='existingWikiWord' href='/nlab/show/diff/limit+point'>limit points</a> (def. <a class='maruku-ref' href='#Convergence'>4</a>).</p> </div> <div class='proof'> <h6 id='proof_3'>Proof</h6> <p>In one direction, assume that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_262' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> is a Hausdorff space, and that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_263' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> is a net in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_264' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> which has limits points <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_265' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>x</mi> <mn>2</mn></msub><mo>∈</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>x_1, x_2 \in X</annotation></semantics></math>. We need to show that then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_266' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub><mo>=</mo><msub><mi>x</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>x_1 = x_2</annotation></semantics></math>.</p> <p>Assume on the contrary that the two points were different, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_267' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub><mo>≠</mo><msub><mi>x</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>x_1 \neq x_2</annotation></semantics></math>. By assumption of Hausdorffness, these would then have disjoint open neighbourhoods <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_268' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub><mo>,</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>U_{x_1}, U_{x_2}</annotation></semantics></math>, i.e. <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_269' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mn>1</mn></msub><mo>∩</mo><msub><mi>U</mi> <mn>2</mn></msub><mo>=</mo><mi>∅</mi></mrow><annotation encoding='application/x-tex'>U_1 \cap U_2 = \emptyset</annotation></semantics></math>. By definition of convergence, there would thus be <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_270' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>a</mi> <mn>2</mn></msub><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>a_1, a_2 \in A</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_271' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mrow><msub><mi>a</mi> <mn>1</mn></msub><mo>≤</mo><mo>•</mo></mrow></msub><mo>∈</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>\nu_{a_1 \leq \bullet} \in U_{x_1}</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_272' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mrow><msub><mi>a</mi> <mn>2</mn></msub><mo>≤</mo><mo>•</mo></mrow></msub><mo>∈</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>\nu_{a_2 \leq \bullet} \in U_{x_2}</annotation></semantics></math>. Moreover, by the definition of directed set, this would imply <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_273' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mn>3</mn></msub><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>a_3 \in A</annotation></semantics></math> with <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_274' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>a</mi> <mn>2</mn></msub><mo>≤</mo><msub><mi>a</mi> <mn>3</mn></msub></mrow><annotation encoding='application/x-tex'>a_1, a_2 \leq a_3</annotation></semantics></math>, and hence that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_275' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mrow><msub><mi>a</mi> <mn>3</mn></msub><mo>≤</mo><mo>•</mo></mrow></msub><mo>∈</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub><mo>∩</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>x_{a_3 \leq \bullet} \in U_{x_1} \cap U_{x_2}</annotation></semantics></math>. This is in contradiction to the emptiness of the intersection, and hence we have a <a class='existingWikiWord' href='/nlab/show/diff/proof+by+contradiction'>proof by contradiction</a>.</p> <p>Conversely, assume that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_276' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> is not a Hausdorff space. We need to show that then there exists a net <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_277' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi></mrow><annotation encoding='application/x-tex'>\nu</annotation></semantics></math> in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_278' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> with two distinct limit points.</p> <p>That <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_279' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> is not Hausdorff means that there are two distinct points <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_280' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>x</mi> <mn>2</mn></msub><mo>∈</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>x_1, x_2 \in X</annotation></semantics></math> such that every open neighbourhood of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_281' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow><annotation encoding='application/x-tex'>x_1</annotation></semantics></math> intersects every open neighbourhood of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_282' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>x_2</annotation></semantics></math>. Hence we may <a class='existingWikiWord' href='/nlab/show/diff/axiom+of+choice'>choose</a> elements in these intersections</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_283' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mrow><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub><mo>,</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow></msub></mrow></msub><mo>∈</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub><mo>,</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow></msub><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> x_{U_{x_1}, U_{x_2}} \in U_{x_1}, U_{x_2} \,. </annotation></semantics></math></div> <p>Consider the directed neighbourhood sets <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_284' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>1</mn></msub><msub><mo stretchy='false'>)</mo> <mo>⊃</mo></msub></mrow><annotation encoding='application/x-tex'>Nbhd_X(x_1)_{\supset}</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_285' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>2</mn></msub><msub><mo stretchy='false'>)</mo> <mo>⊃</mo></msub></mrow><annotation encoding='application/x-tex'>Nbhd_X(x_2)_{\supset}</annotation></semantics></math> of these two points (example <a class='maruku-ref' href='#DirectedSetOfNeighbourhods'>2</a>) and their directed Cartesian product set (example <a class='maruku-ref' href='#DirectedProductSet'>3</a>) <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_286' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>1</mn></msub><msub><mo stretchy='false'>)</mo> <mo>⊃</mo></msub><mo>×</mo><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>2</mn></msub><msub><mo stretchy='false'>)</mo> <mo>⊃</mo></msub></mrow><annotation encoding='application/x-tex'>Nbhd_X(x_1)_{\supset} \times Nbhd_X(x_2)_{\supset}</annotation></semantics></math>. The above elements then define a net</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_287' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable><mtr><mtd><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo><mo>×</mo><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo></mtd> <mtd><mover><mo>⟶</mo><mi>ν</mi></mover></mtd> <mtd><mi>X</mi></mtd></mtr> <mtr><mtd><mo stretchy='false'>(</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub><mo>,</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow></msub><mo stretchy='false'>)</mo></mtd> <mtd><mover><mo>↦</mo><mphantom><mi>AAA</mi></mphantom></mover></mtd> <mtd><msub><mi>x</mi> <mrow><msub><mi>U</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>U</mi> <mn>2</mn></msub></mrow></msub></mtd></mtr></mtable></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> \array{ Nbhd_X(x_1) \times Nbhd_X(x_2) &\overset{\nu}{\longrightarrow}& X \\ (U_{x_1}, U_{x_2}) &\overset{\phantom{AAA}}{\mapsto}& x_{U_1, U_2} } \,. </annotation></semantics></math></div> <p>We conclude by claiming that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_288' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow><annotation encoding='application/x-tex'>x_1</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_289' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>x_2</annotation></semantics></math> are both limit points of this net. We show this for <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_290' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow><annotation encoding='application/x-tex'>x_1</annotation></semantics></math>, the argument for <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_291' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>x_2</annotation></semantics></math> is directly analogous:</p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_292' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>U_{x_1}</annotation></semantics></math> be an open neighbourhood of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_293' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow><annotation encoding='application/x-tex'>x_1</annotation></semantics></math>. We need to find an element <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_294' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>V</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>V</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo><mo>∈</mo><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo><mo>×</mo><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><msub><mi>x</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(V_1, V_2) \in Nbhd_X(x_1) \times Nbhd_X(x_2)</annotation></semantics></math> such that for all <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_295' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>W</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>W</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo><mo>⊂</mo><mo stretchy='false'>(</mo><msub><mi>V</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>V</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(W_1, W_2) \subset (V_1, V_2)</annotation></semantics></math> then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_296' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mrow><mo stretchy='false'>(</mo><msub><mi>W</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>W</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo></mrow></msub><mo>∈</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>\nu_{(W_1, W_2)} \in U_{x_1}</annotation></semantics></math>.</p> <p>Take <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_297' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>V</mi> <mn>1</mn></msub><mo>≔</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>V_1 \coloneqq U_{x_1}</annotation></semantics></math> and take <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_298' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>V</mi> <mn>2</mn></msub><mo>=</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>V_2 = X</annotation></semantics></math>. Then by construction</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_299' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable columnalign='right left right left right left right left right left' columnspacing='0em' displaystyle='true'><mtr><mtd><msub><mi>ν</mi> <mrow><mo stretchy='false'>(</mo><msub><mi>W</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>W</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo></mrow></msub></mtd> <mtd><mo>∈</mo><msub><mi>W</mi> <mn>1</mn></msub><mo>∩</mo><msub><mi>W</mi> <mn>2</mn></msub></mtd></mtr> <mtr><mtd /> <mtd><mo>⊂</mo><msub><mi>V</mi> <mn>1</mn></msub><mo>∩</mo><msub><mi>V</mi> <mn>2</mn></msub></mtd></mtr> <mtr><mtd /> <mtd><mo>=</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub><mo>∩</mo><mi>X</mi></mtd></mtr> <mtr><mtd /> <mtd><mo>=</mo><msub><mi>U</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow></msub></mtd></mtr></mtable></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> \begin{aligned} \nu_{(W_1, W_2)} & \in W_1 \cap W_2 \\ & \subset V_1 \cap V_2 \\ & = U_{x_1} \cap X \\ & = U_{x_1} \end{aligned} \,. </annotation></semantics></math></div></div> <div class='num_prop' id='CompactSpacesEquivalentlyHaveConvergetSubnets'> <h6 id='proposition_5'>Proposition</h6> <p><strong>(<a class='existingWikiWord' href='/nlab/show/diff/compact+spaces+equivalently+have+converging+subnets'>compact spaces are equivalently those for which every net has a converging subnet</a>)</strong></p> <p>Assuming <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a> and the <a class='existingWikiWord' href='/nlab/show/diff/axiom+of+choice'>axiom of choice</a>, then:</p> <p>A <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_300' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> is <a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compact</a> precisely if every <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a> in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_301' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> (def. <a class='maruku-ref' href='#Net'>2</a>) has a <a class='existingWikiWord' href='/nlab/show/diff/subnet'>sub-net</a> (def. <a class='maruku-ref' href='#Willard'>5</a>) that <a class='existingWikiWord' href='/nlab/show/diff/convergence'>converges</a> (def. <a class='maruku-ref' href='#Convergence'>4</a>).</p> </div> <p>We break up the <strong>proof</strong> into that of lemmas <a class='maruku-ref' href='#InACompactSpaceEveryNetHasAConvergentSubnet'>5</a> and <a class='maruku-ref' href='#IfEveryNetHasConvergentSubnetThenSpaceIsCompact'>6</a>:</p> <div class='num_example' id='InACompactSpaceEveryNetHasAConvergentSubnet'> <h6 id='lemma'>Lemma</h6> <p><strong>(in a compact space, every net has a convergent subnet)</strong></p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_302' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compact topological space</a>. Then every net in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_303' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> has a convergent subnet.</p> </div> <div class='proof'> <h6 id='proof_4'>Proof</h6> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_304' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo lspace='verythinmathspace'>:</mo><mi>A</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>\nu \colon A \to X</annotation></semantics></math> be a net. We need to show that there is a subnet which converges.</p> <p>For <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_305' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>a \in A</annotation></semantics></math> consider the <a class='existingWikiWord' href='/nlab/show/diff/closed+subspace'>topological closures</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_306' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Cl</mi><mo stretchy='false'>(</mo><msub><mi>S</mi> <mi>a</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>Cl(S_a)</annotation></semantics></math> of the sets <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_307' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>S</mi> <mi>a</mi></msub></mrow><annotation encoding='application/x-tex'>S_a</annotation></semantics></math> of elements of the net beyond some fixed index:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_308' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>S</mi> <mi>a</mi></msub><mspace width='thickmathspace' /><mo>≔</mo><mspace width='thickmathspace' /><mrow><mo>{</mo><msub><mi>ν</mi> <mi>b</mi></msub><mo>∈</mo><mi>X</mi><mspace width='thickmathspace' /><mo stretchy='false'>|</mo><mspace width='thickmathspace' /><mi>b</mi><mo>≥</mo><mi>a</mi><mo>}</mo></mrow><mo>⊂</mo><mi>X</mi><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> S_a \;\coloneqq\; \left\{ \nu_b \in X \;\vert\; b \geq a \right\} \subset X \,. </annotation></semantics></math></div> <p>Observe that the set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_309' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>{</mo><msub><mi>S</mi> <mi>a</mi></msub><mo>⊂</mo><mi>X</mi><msub><mo stretchy='false'>}</mo> <mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow></msub></mrow><annotation encoding='application/x-tex'>\{S_a \subset X\}_{a \in A}</annotation></semantics></math> and hence also the set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_310' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>{</mo><mi>Cl</mi><mo stretchy='false'>(</mo><msub><mi>S</mi> <mi>a</mi></msub><mo stretchy='false'>)</mo><mo>⊂</mo><mi>X</mi><msub><mo stretchy='false'>}</mo> <mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow></msub></mrow><annotation encoding='application/x-tex'>\{Cl(S_a) \subset X\}_{a \in A}</annotation></semantics></math> has the <a class='existingWikiWord' href='/nlab/show/diff/finite+intersection+property'>finite intersection property</a>, by the fact that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_311' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a>. Therefore <a href='finite+intersection+property#CompactnessInTermsOfFiniteIntersectionProperty'>this prop.</a> implies from the assumption of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_312' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> being compact that the intersection of <em>all</em> the <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_313' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Cl</mi><mo stretchy='false'>(</mo><msub><mi>S</mi> <mi>a</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>Cl(S_a)</annotation></semantics></math> is non-empty, hence that there is an element</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_314' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><munder><mo>∩</mo><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow></munder><mi>Cl</mi><mo stretchy='false'>(</mo><msub><mi>S</mi> <mi>a</mi></msub><mo stretchy='false'>)</mo><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> x \in \underset{a \in A}{\cap} Cl(S_a) \,. </annotation></semantics></math></div> <p>In particular every <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhood</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_315' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>U_x</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_316' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> intersects each of the <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_317' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Cl</mi><mo stretchy='false'>(</mo><msub><mi>S</mi> <mi>a</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>Cl(S_a)</annotation></semantics></math>, and hence also each of the <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_318' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>S</mi> <mi>a</mi></msub></mrow><annotation encoding='application/x-tex'>S_a</annotation></semantics></math>. By definition of the <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_319' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>S</mi> <mi>a</mi></msub></mrow><annotation encoding='application/x-tex'>S_a</annotation></semantics></math>, this means that for every <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_320' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding='application/x-tex'>a \in A</annotation></semantics></math> there exists <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_321' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>b</mi><mo>≥</mo><mi>a</mi></mrow><annotation encoding='application/x-tex'>b \geq a</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_322' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mi>b</mi></msub><mo>∈</mo><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>\nu_b \in U_x</annotation></semantics></math>, hence that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_323' 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 <a class='existingWikiWord' href='/nlab/show/diff/limit+point'>cluster point</a> (def <a class='maruku-ref' href='#Convergence'>4</a>) of the net.</p> <p>We will now produce a <a class='existingWikiWord' href='/nlab/show/diff/subnet'>sub-net</a></p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_324' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable><mtr><mtd><mi>B</mi></mtd> <mtd /> <mtd><mover><mo>⟶</mo><mi>f</mi></mover></mtd> <mtd /> <mtd><mi>A</mi></mtd></mtr> <mtr><mtd /> <mtd><mo>↘</mo></mtd> <mtd /> <mtd><msub><mo>↙</mo> <mi>ν</mi></msub></mtd></mtr> <mtr><mtd /> <mtd /> <mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding='application/x-tex'> \array{ B && \overset{f}{\longrightarrow} && A \\ & \searrow && \swarrow_{\nu} \\ && X } </annotation></semantics></math></div> <p>that converges to this cluster point. To this end, we first need to build the domain directed set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_325' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math>. Take it to be the sub-directed set of the Cartesian product directed set (example <a class='maruku-ref' href='#DirectedProductSet'>3</a>) of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_326' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> with the directed neighbourhood set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_327' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>Nbhd_X(x)</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_328' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> (example <a class='maruku-ref' href='#DirectedSetOfNeighbourhods'>2</a>)</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_329' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi><mo>⊂</mo><msub><mi>A</mi> <mo>≤</mo></msub><mo>×</mo><msub><mi>Nbhd</mi> <mi>X</mi></msub><mo stretchy='false'>(</mo><mi>x</mi><msub><mo stretchy='false'>)</mo> <mo>⊃</mo></msub></mrow><annotation encoding='application/x-tex'> B \subset A_{\leq} \times Nbhd_X(x)_{\supset} </annotation></semantics></math></div> <p>on those pairs such that the element of the net indexed by the first component is contained in the second component:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_330' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi><mspace width='thickmathspace' /><mo>≔</mo><mspace width='thickmathspace' /><mrow><mo>{</mo><mo stretchy='false'>(</mo><mi>a</mi><mo>,</mo><msub><mi>U</mi> <mi>x</mi></msub><mo stretchy='false'>)</mo><mspace width='thinmathspace' /><mo stretchy='false'>|</mo><mspace width='thinmathspace' /><msub><mi>ν</mi> <mi>a</mi></msub><mo>∈</mo><msub><mi>U</mi> <mi>X</mi></msub><mo>}</mo></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> B \;\coloneqq\; \left\{ (a,U_x) \,\vert \, \nu_a \in U_X \right\} \,. </annotation></semantics></math></div> <p>It is clear <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_331' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/preorder'>preordered set</a>. We need to check that it is indeed directed, in that every pair of elements <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_332' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>a</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>U</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(a_1, U_1)</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_333' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>a</mi> <mn>2</mn></msub><mo>,</mo><msub><mi>U</mi> <mn>2</mn></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(a_2, U_2)</annotation></semantics></math> has a common upper bound <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_334' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><msub><mi>a</mi> <mi>bd</mi></msub><mo>,</mo><msub><mi>U</mi> <mi>bd</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(a_{bd}, U_{bd})</annotation></semantics></math>. Now since <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_335' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>A</mi></mrow><annotation encoding='application/x-tex'>A</annotation></semantics></math> itself is directed, there is an upper bound <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_336' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mn>3</mn></msub><mo>≥</mo><msub><mi>a</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>a</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>a_3 \geq a_1, a_2</annotation></semantics></math>, and since <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_337' 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 cluster point of the net there is moreover an <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_338' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mi>bd</mi></msub><mo>≥</mo><msub><mi>a</mi> <mn>3</mn></msub><mo>≥</mo><msub><mi>a</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>a</mi> <mn>3</mn></msub></mrow><annotation encoding='application/x-tex'>a_{bd} \geq a_3 \geq a_1, a_3</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_339' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mrow><msub><mi>a</mi> <mi>bd</mi></msub></mrow></msub><mo>∈</mo><msub><mi>U</mi> <mn>1</mn></msub><mo>∩</mo><msub><mi>U</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>\nu_{a_{bd}} \in U_1 \cap U_2</annotation></semantics></math>. Hence with <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_340' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mi>bd</mi></msub><mo>≔</mo><msub><mi>U</mi> <mn>1</mn></msub><mo>∩</mo><msub><mi>U</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>U_{bd} \coloneqq U_1 \cap U_2</annotation></semantics></math> we have obtained the required pair.</p> <p>Next take the function <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_341' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> to be given by</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_342' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable><mtr><mtd><mi>B</mi></mtd> <mtd><mover><mo>⟶</mo><mi>f</mi></mover></mtd> <mtd><mi>A</mi></mtd></mtr> <mtr><mtd><mo stretchy='false'>(</mo><mi>a</mi><mo>,</mo><mi>U</mi><mo stretchy='false'>)</mo></mtd> <mtd><mover><mo>↦</mo><mphantom><mi>AAA</mi></mphantom></mover></mtd> <mtd><mi>a</mi></mtd></mtr></mtable></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> \array{ B &\overset{f}{\longrightarrow}& A \\ (a, U) &\overset{\phantom{AAA}}{\mapsto}& a } \,. </annotation></semantics></math></div> <p>This is clearly order preserving, and it is cofinal since it is even a surjection. Hence we have defined a subnet <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_343' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo>∘</mo><mi>f</mi></mrow><annotation encoding='application/x-tex'>\nu \circ f</annotation></semantics></math>.</p> <p>It now remains to see that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_344' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo>∘</mo><mi>f</mi></mrow><annotation encoding='application/x-tex'>\nu \circ f</annotation></semantics></math> converges to <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_345' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math>, hence that for every open neighbourhood <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_346' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>U_x</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_347' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> we may find <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_348' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>a</mi><mo>,</mo><mi>U</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(a,U)</annotation></semantics></math> such that for all <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_349' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>b</mi><mo>,</mo><mi>V</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(b,V)</annotation></semantics></math> with <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_350' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>≤</mo><mi>b</mi></mrow><annotation encoding='application/x-tex'>a \leq b</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_351' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi><mo>⊃</mo><mi>V</mi></mrow><annotation encoding='application/x-tex'>U \supset V</annotation></semantics></math> then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_352' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ν</mi><mo stretchy='false'>(</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>b</mi><mo>,</mo><mi>V</mi><mo stretchy='false'>)</mo><mo stretchy='false'>)</mo><mo>=</mo><mi>ν</mi><mo stretchy='false'>(</mo><mi>b</mi><mo stretchy='false'>)</mo><mo>∈</mo><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>\nu(f(b,V)) = \nu(b) \in U_x</annotation></semantics></math>. Now by the nature of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_353' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> there exists some <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_354' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi></mrow><annotation encoding='application/x-tex'>a</annotation></semantics></math> with <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_355' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mi>a</mi></msub><mo>∈</mo><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>\nu_a \in U_x</annotation></semantics></math>, and hence if we take <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_356' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi><mo>≔</mo><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>U \coloneqq U_x</annotation></semantics></math> then nature of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_357' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> implies that with <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_358' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>b</mi><mo>,</mo><mi>V</mi><mo stretchy='false'>)</mo><mo>≥</mo><mo stretchy='false'>(</mo><mi>a</mi><mo>,</mo><msub><mi>U</mi> <mi>x</mi></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(b, V) \geq (a,U_x)</annotation></semantics></math> then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_359' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi><mo>⊂</mo><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>b \in V \subset U_x</annotation></semantics></math>.</p> </div> <div class='num_example' id='IfEveryNetHasConvergentSubnetThenSpaceIsCompact'> <h6 id='lemma_2'>Lemma</h6> <p>Assuming <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a>, then:</p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_360' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topological space</a>. If every <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a> in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_361' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> has a <a class='existingWikiWord' href='/nlab/show/diff/subnet'>subnet</a> that <a class='existingWikiWord' href='/nlab/show/diff/convergence'>converges</a>, then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_362' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compact topological space</a>.</p> </div> <div class='proof'> <h6 id='proof_5'>Proof</h6> <p>By <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a> we may equivalently prove the <a class='existingWikiWord' href='/nlab/show/diff/contrapositive'>contrapositive</a>: If <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_363' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> is not compact, then not every net in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_364' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> has a convergent subnet.</p> <p>Hence assume that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_365' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> is not compact. We need to produce a net without a convergent subnet.</p> <p>Again by <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a>, then by <a href='finite+intersection+property#CompactnessInTermsOfFiniteIntersectionProperty'>this prop.</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_366' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>X</mi><mo>,</mo><mi>τ</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(X,\tau)</annotation></semantics></math> not being compact means equivalently that there exists a set <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_367' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>{</mo><msub><mi>C</mi> <mi>i</mi></msub><mo>⊂</mo><mi>X</mi><msub><mo stretchy='false'>}</mo> <mrow><mi>i</mi><mo>∈</mo><mi>I</mi></mrow></msub></mrow><annotation encoding='application/x-tex'>\{C_i \subset X\}_{i \in I}</annotation></semantics></math> of <a class='existingWikiWord' href='/nlab/show/diff/closed+subspace'>closed subsets</a> satisfying the <a class='existingWikiWord' href='/nlab/show/diff/finite+intersection+property'>finite intersection property</a>, but such that their intersection is empty: <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_368' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><munder><mo>∩</mo><mrow><mi>i</mi><mo>∈</mo><mi>I</mi></mrow></munder><msub><mi>C</mi> <mi>i</mi></msub><mo>=</mo><mi>∅</mi></mrow><annotation encoding='application/x-tex'>\underset{i \in I}{\cap} C_i = \emptyset</annotation></semantics></math>.</p> <p>Consider then <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_369' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>P</mi> <mi>fin</mi></msub><mo stretchy='false'>(</mo><mi>I</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>P_{fin}(I)</annotation></semantics></math>, the set of <a class='existingWikiWord' href='/nlab/show/diff/finite+set'>finite</a> <a class='existingWikiWord' href='/nlab/show/diff/subset'>subsets</a> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_370' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>I</mi></mrow><annotation encoding='application/x-tex'>I</annotation></semantics></math>. By the assumption that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_371' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>{</mo><msub><mi>C</mi> <mi>i</mi></msub><mo>⊂</mo><mi>X</mi><msub><mo stretchy='false'>}</mo> <mrow><mi>i</mi><mo>∈</mo><mi>I</mi></mrow></msub></mrow><annotation encoding='application/x-tex'>\{C_i \subset X\}_{i \in I}</annotation></semantics></math> satisfies the <a class='existingWikiWord' href='/nlab/show/diff/finite+intersection+property'>finite intersection property</a>, we may <a class='existingWikiWord' href='/nlab/show/diff/axiom+of+choice'>choose</a> for each <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_372' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>J</mi><mo>∈</mo><msub><mi>P</mi> <mi>fin</mi></msub><mo stretchy='false'>(</mo><mi>I</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>J \in P_{fin}(I)</annotation></semantics></math> an element</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_373' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mi>J</mi></msub><mo>∈</mo><munder><mo>∩</mo><mrow><mi>i</mi><mo>∈</mo><mi>J</mi><mo>⊂</mo><mi>I</mi></mrow></munder><msub><mi>C</mi> <mi>i</mi></msub><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> x_J \in \underset{i \in J \subset I}{\cap} C_i \,. </annotation></semantics></math></div> <p>Now <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_374' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>P</mi> <mi>fin</mi></msub><mo stretchy='false'>(</mo><mi>X</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>P_{fin}(X)</annotation></semantics></math> regarded as a <a class='existingWikiWord' href='/nlab/show/diff/preorder'>preordered set</a> under inclusion of subsets is clearly a <a class='existingWikiWord' href='/nlab/show/diff/direction'>directed set</a>, with an upper bound of two finite subsets given by their <a class='existingWikiWord' href='/nlab/show/diff/union'>union</a>. Therefore we have defined a net</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_375' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable><mtr><mtd><msub><mi>P</mi> <mi>fin</mi></msub><mo stretchy='false'>(</mo><mi>X</mi><msub><mo stretchy='false'>)</mo> <mo>⊂</mo></msub></mtd> <mtd><mover><mo>⟶</mo><mi>ν</mi></mover></mtd> <mtd><mi>X</mi></mtd></mtr> <mtr><mtd><mi>J</mi></mtd> <mtd><mover><mo>↦</mo><mphantom><mi>AAA</mi></mphantom></mover></mtd> <mtd><msub><mi>x</mi> <mi>J</mi></msub></mtd></mtr></mtable></mrow><mspace width='thinmathspace' /><mo>.</mo></mrow><annotation encoding='application/x-tex'> \array{ P_{fin}(X)_{\subset} &\overset{\nu}{\longrightarrow}& X \\ J &\overset{\phantom{AAA}}{\mapsto}& x_J } \,. </annotation></semantics></math></div> <p>We will show that this net has no converging subnet.</p> <p>Assume on the contrary that there were a subnet</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_376' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mtable><mtr><mtd><mi>B</mi></mtd> <mtd /> <mtd><mover><mo>⟶</mo><mi>f</mi></mover></mtd> <mtd /> <mtd><msub><mi>P</mi> <mi>fin</mi></msub><mo stretchy='false'>(</mo><mi>X</mi><mo stretchy='false'>)</mo></mtd></mtr> <mtr><mtd /> <mtd><mo>↘</mo></mtd> <mtd /> <mtd><msub><mo>↙</mo> <mi>ν</mi></msub></mtd></mtr> <mtr><mtd /> <mtd /> <mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding='application/x-tex'> \array{ B && \overset{f}{\longrightarrow} && P_{fin}(X) \\ & \searrow && \swarrow_{\nu} \\ && X } </annotation></semantics></math></div> <p>which converges to some <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_377' 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>.</p> <p>By the assumption that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_378' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><munder><mo>∩</mo><mrow><mi>i</mi><mo>∈</mo><mi>I</mi></mrow></munder><msub><mi>C</mi> <mi>i</mi></msub><mo>=</mo><mi>∅</mi></mrow><annotation encoding='application/x-tex'>\underset{i \in I}{\cap} C_i = \emptyset</annotation></semantics></math>, there would exist an <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_379' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>i</mi> <mi>x</mi></msub><mo>∈</mo><mi>I</mi></mrow><annotation encoding='application/x-tex'>i_x \in I</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_380' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>≠</mo><msub><mi>C</mi> <mrow><msub><mi>i</mi> <mi>x</mi></msub></mrow></msub></mrow><annotation encoding='application/x-tex'>x \neq C_{i_x}</annotation></semantics></math>, and because <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_381' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>C</mi> <mi>i</mi></msub></mrow><annotation encoding='application/x-tex'>C_i</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/closed+subspace'>closed subset</a>, there would exist even an <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>open neighbourhood</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_382' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>U_x</annotation></semantics></math> of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_383' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi></mrow><annotation encoding='application/x-tex'>x</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_384' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mi>x</mi></msub><mo>∩</mo><msub><mi>C</mi> <mrow><msub><mi>i</mi> <mi>x</mi></msub></mrow></msub><mo>=</mo><mi>∅</mi></mrow><annotation encoding='application/x-tex'>U_x \cap C_{i_x} = \emptyset</annotation></semantics></math>. This would imply that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_385' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>x</mi> <mi>J</mi></msub><mo>≠</mo><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>x_J \neq U_x</annotation></semantics></math> for all <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_386' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>J</mi><mo>⊃</mo><mo stretchy='false'>{</mo><msub><mi>i</mi> <mi>x</mi></msub><mo stretchy='false'>}</mo></mrow><annotation encoding='application/x-tex'>J \supset \{i_x\}</annotation></semantics></math>.</p> <p>Now since the function <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_387' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> defining the subset is cofinal, there would exist <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_388' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>b</mi> <mn>1</mn></msub><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>b_1 \in B</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_389' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>{</mo><msub><mi>i</mi> <mi>x</mi></msub><mo stretchy='false'>}</mo><mo>⊂</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>b</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\{i_x\} \subset f(b_1)</annotation></semantics></math>. Moreover, by the assumption that the subnet converges, there would also be <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_390' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>b</mi> <mn>2</mn></msub><mo>∈</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>b_2 \in B</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_391' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mrow><msub><mi>b</mi> <mn>2</mn></msub><mo>≤</mo><mo>•</mo></mrow></msub><mo>∈</mo><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>\nu_{b_2 \leq \bullet} \in U_x</annotation></semantics></math>. Since <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_392' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math> is directed, there would then be an upper bound <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_393' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>b</mi><mo>≥</mo><msub><mi>b</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>b</mi> <mn>2</mn></msub></mrow><annotation encoding='application/x-tex'>b \geq b_1, b_2</annotation></semantics></math> of these two elements. This hence satisfies both <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_394' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>e</mi><mo stretchy='false'>)</mo></mrow></msub><mo>∈</mo><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>\nu_{f(e)} \in U_x</annotation></semantics></math> as well as <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_395' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>{</mo><msub><mi>i</mi> <mi>x</mi></msub><mo stretchy='false'>}</mo><mo>⊂</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>b</mi> <mn>1</mn></msub><mo stretchy='false'>)</mo><mo>⊂</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>b</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>\{i_x\} \subset f(b_1) \subset f(b)</annotation></semantics></math>. But the latter of these two means that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_396' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>ν</mi> <mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>b</mi><mo stretchy='false'>)</mo></mrow></msub></mrow><annotation encoding='application/x-tex'>\nu_{f(b)}</annotation></semantics></math> is not in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_397' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding='application/x-tex'>U_x</annotation></semantics></math>, which is a contradiction to the former. Thus we have a <a class='existingWikiWord' href='/nlab/show/diff/proof+by+contradiction'>proof by contradiction</a>.</p> </div> <h3 id='LogicOfNets'>Logic of nets</h3> <p>A <a class='existingWikiWord' href='/nlab/show/diff/stuff%2C+structure%2C+property'>property</a> of <a class='existingWikiWord' href='/nlab/show/diff/element'>elements</a> of a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_398' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> (given by the <a class='existingWikiWord' href='/nlab/show/diff/subset'>subset</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_399' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi><mo>⊂</mo><mi>X</mi></mrow><annotation encoding='application/x-tex'>S \subset X</annotation></semantics></math> of those elements of <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_400' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> satisfying this property) may be applied to nets in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_401' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>.</p> <p>Being eventually in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_402' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>, def. <a class='maruku-ref' href='#EventuallyAndFrequently'>3</a>, is a weakening of being always in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_403' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> (given by the <a class='existingWikiWord' href='/nlab/show/diff/universal+quantifier'>universal quantifier</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_404' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mo>∀</mo> <mi>ν</mi></msub></mrow><annotation encoding='application/x-tex'>\forall_\nu</annotation></semantics></math>), while being frequently in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_405' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> is a strengthening of being sometime in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_406' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math> (given by the <a class='existingWikiWord' href='/nlab/show/diff/existential+quantifier'>particular quantifier</a> <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_407' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mo>∃</mo> <mi>ν</mi></msub></mrow><annotation encoding='application/x-tex'>\exists_\nu</annotation></semantics></math>). Indeed we can build a <a class='existingWikiWord' href='/nlab/show/diff/formal+logic'>formal logic</a> out of these. Use <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_408' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><mo>∀</mo><mi>i</mi><mo>,</mo><mi>p</mi><mo stretchy='false'>[</mo><msub><mi>ν</mi> <mi>i</mi></msub><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>\ess\forall i, p[\nu_i]</annotation></semantics></math> or <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_409' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mi>p</mi></mrow><annotation encoding='application/x-tex'>\ess\forall_\nu p</annotation></semantics></math> to mean that a predicate <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_410' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi></mrow><annotation encoding='application/x-tex'>p</annotation></semantics></math> in <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_411' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math> is eventually true, and use <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_412' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><mo>∃</mo><mi>i</mi><mo>,</mo><mi>p</mi><mo stretchy='false'>[</mo><msub><mi>ν</mi> <mi>i</mi></msub><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>\ess\exists i, p[\nu_i]</annotation></semantics></math> or <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_413' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mi>p</mi></mrow><annotation encoding='application/x-tex'>\ess\exists_\nu p</annotation></semantics></math> to mean that <math class='maruku-mathml' display='inline' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_414' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi></mrow><annotation encoding='application/x-tex'>p</annotation></semantics></math> is frequently true. Then we have:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_415' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mo>∀</mo> <mi>ν</mi></msub><mi>p</mi><mspace width='thickmathspace' /><mo>⇒</mo><mspace width='thickmathspace' /><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mi>p</mi><mspace width='thickmathspace' /><mo>⇒</mo><mspace width='thickmathspace' /><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mi>p</mi><mspace width='thickmathspace' /><mo>⇒</mo><mspace width='thickmathspace' /><msub><mo>∃</mo> <mi>ν</mi></msub><mi>p</mi></mrow><annotation encoding='application/x-tex'>\forall_\nu p \;\Rightarrow\; \ess\forall_\nu p \;\Rightarrow\; \ess\exists_\nu p \;\Rightarrow\; \exists_\nu p</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_416' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mo stretchy='false'>(</mo><mi>p</mi><mo>∧</mo><mi>q</mi><mo stretchy='false'>)</mo><mspace width='thickmathspace' /><mo>⇔</mo><mspace width='thickmathspace' /><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mi>p</mi><mo>∧</mo><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mi>q</mi></mrow><annotation encoding='application/x-tex'>\ess\forall_\nu (p \wedge q) \;\Leftrightarrow\; \ess\forall_\nu p \wedge \ess\forall_\nu q</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_417' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mo stretchy='false'>(</mo><mi>p</mi><mo>∧</mo><mi>q</mi><mo stretchy='false'>)</mo><mspace width='thickmathspace' /><mo>⇒</mo><mspace width='thickmathspace' /><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mi>p</mi><mo>∧</mo><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mi>q</mi></mrow><annotation encoding='application/x-tex'>\ess\exists_\nu (p \wedge q) \;\Rightarrow\; \ess\exists_\nu p \wedge \ess\exists_\nu q</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_418' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mo stretchy='false'>(</mo><mi>p</mi><mo>∨</mo><mi>q</mi><mo stretchy='false'>)</mo><mspace width='thickmathspace' /><mo>⇐</mo><mspace width='thickmathspace' /><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mi>p</mi><mo>∧</mo><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mi>q</mi></mrow><annotation encoding='application/x-tex'>\ess\forall_\nu (p \vee q) \;\Leftarrow\; \ess\forall_\nu p \wedge \ess\forall_\nu q</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_419' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mo stretchy='false'>(</mo><mi>p</mi><mo>∨</mo><mi>q</mi><mo stretchy='false'>)</mo><mspace width='thickmathspace' /><mo>⇔</mo><mspace width='thickmathspace' /><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mi>p</mi><mo>∨</mo><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mi>q</mi></mrow><annotation encoding='application/x-tex'>\ess\exists_\nu (p \vee q) \;\Leftrightarrow\; \ess\exists_\nu p \vee \ess\exists_\nu q</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0c09b5b4f42a37589ae4de8ac2d7afc86feac23a_420' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mo>¬</mo><mi>p</mi><mspace width='thickmathspace' /><mo>⇔</mo><mspace width='thickmathspace' /><mo>¬</mo><mo lspace='0em' rspace='thinmathspace'>ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mi>p</mi></mrow><annotation encoding='application/x-tex'>\ess\forall_\nu \neg{p} \;\Leftrightarrow\; \neg\ess\exists_\nu p</annotation></semantics></math></div> <p>and other analogues of theorems from <a class='existingWikiWord' href='/nlab/show/diff/predicate+logic'>predicate logic</a>. Note that the last item listed requires <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a> even though its analogue from ordinary predicate logic does not.</p> <p>A similar logic is satisfied by ‘<a class='existingWikiWord' href='/nlab/show/diff/null+subset'>almost everywhere</a>’ and its dual (‘not almost nowhere’ or ‘somewhere significant’) in <a class='existingWikiWord' href='/nlab/show/diff/measure+space'>measure spaces</a>.</p> <h2 id='related_concepts'>Related concepts</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/sequential+net'>sequential net</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/convergence'>limit of a net</a></p> </li> <li> <p><a href='Tychonoff+theorem#ProofViaNets'>Tychonoff theorem – Proof via net convergence</a></p> </li> </ul> <h2 id='references'>References</h2> <p>A textbook account is in</p> <ul> <li id='Schechter96'><a class='existingWikiWord' href='/nlab/show/diff/Eric+Schechter'>Eric Schechter</a>, sections 7.14–7.21 of <em><a class='existingWikiWord' href='/nlab/show/diff/Handbook+of+Analysis+and+its+Foundations'>Handbook of Analysis and its Foundations</a></em>, Academic Press (1996)</li> </ul> <p>Lecture notes include</p> <ul> <li id='Vermeeren10'><a class='existingWikiWord' href='/nlab/show/diff/Stijn+Vermeeren'>Stijn Vermeeren</a>, <em>Sequences and nets in topology</em>, 2010 (<a href='http://stijnvermeeren.be/download/mathematics/nets.pdf'>pdf</a>)</li> </ul> <p> </p> </div> <div class="revisedby"> <p> Last revised on November 11, 2024 at 17:32:24. See the <a href="/nlab/history/net" 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/net" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/11009/#Item_2">Discuss</a><span class="backintime"><a href="/nlab/revision/diff/net/38" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/net" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Hide changes</a><a href="/nlab/history/net" accesskey="S" class="navlink" id="history" rel="nofollow">History (38 revisions)</a> <a href="/nlab/show/net/cite" style="color: black">Cite</a> <a href="/nlab/print/net" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/net" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>