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 in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <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 </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/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"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="topology">Topology</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/topology">topology</a></strong> (<a class="existingWikiWord" href="/nlab/show/point-set+topology">point-set topology</a>, <a class="existingWikiWord" href="/nlab/show/point-free+topology">point-free topology</a>)</p> <p>see also <em><a class="existingWikiWord" href="/nlab/show/differential+topology">differential topology</a></em>, <em><a class="existingWikiWord" href="/nlab/show/algebraic+topology">algebraic topology</a></em>, <em><a class="existingWikiWord" href="/nlab/show/functional+analysis">functional analysis</a></em> and <em><a class="existingWikiWord" href="/nlab/show/topological+homotopy+theory">topological</a> <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a></em></p> <p><a class="existingWikiWord" href="/nlab/show/Introduction+to+Topology">Introduction</a></p> <p><strong>Basic concepts</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/open+subset">open subset</a>, <a class="existingWikiWord" href="/nlab/show/closed+subset">closed subset</a>, <a class="existingWikiWord" href="/nlab/show/neighbourhood">neighbourhood</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a>, <a class="existingWikiWord" href="/nlab/show/locale">locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/base+for+the+topology">base for the topology</a>, <a class="existingWikiWord" href="/nlab/show/neighbourhood+base">neighbourhood base</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/finer+topology">finer/coarser topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+closure">closure</a>, <a class="existingWikiWord" href="/nlab/show/topological+interior">interior</a>, <a class="existingWikiWord" href="/nlab/show/topological+boundary">boundary</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/separation+axiom">separation</a>, <a class="existingWikiWord" href="/nlab/show/sober+topological+space">sobriety</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/continuous+function">continuous function</a>, <a class="existingWikiWord" href="/nlab/show/homeomorphism">homeomorphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/uniformly+continuous+function">uniformly continuous function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+embedding">embedding</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/open+map">open map</a>, <a class="existingWikiWord" href="/nlab/show/closed+map">closed map</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sequence">sequence</a>, <a class="existingWikiWord" href="/nlab/show/net">net</a>, <a class="existingWikiWord" href="/nlab/show/sub-net">sub-net</a>, <a class="existingWikiWord" href="/nlab/show/filter">filter</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/convergence">convergence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a><a class="existingWikiWord" href="/nlab/show/Top">Top</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/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/initial+topology">initial topology</a>, <a class="existingWikiWord" href="/nlab/show/final+topology">final topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/subspace">subspace</a>, <a class="existingWikiWord" href="/nlab/show/quotient+space">quotient space</a>,</p> </li> <li> <p>fiber space, <a class="existingWikiWord" href="/nlab/show/space+attachment">space attachment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/product+space">product space</a>, <a class="existingWikiWord" href="/nlab/show/disjoint+union+space">disjoint union space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+cylinder">mapping cylinder</a>, <a class="existingWikiWord" href="/nlab/show/mapping+cocylinder">mapping cocylinder</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+cone">mapping cone</a>, <a class="existingWikiWord" href="/nlab/show/mapping+cocone">mapping cocone</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+telescope">mapping telescope</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/colimits+of+normal+spaces">colimits of normal spaces</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/stuff%2C+structure%2C+property">Extra stuff, structure, properties</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/nice+topological+space">nice topological space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/metric+space">metric space</a>, <a class="existingWikiWord" href="/nlab/show/metric+topology">metric topology</a>, <a class="existingWikiWord" href="/nlab/show/metrisable+space">metrisable space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kolmogorov+space">Kolmogorov space</a>, <a class="existingWikiWord" href="/nlab/show/Hausdorff+space">Hausdorff space</a>, <a class="existingWikiWord" href="/nlab/show/regular+space">regular space</a>, <a class="existingWikiWord" href="/nlab/show/normal+space">normal space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sober+space">sober space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+space">compact space</a>, <a class="existingWikiWord" href="/nlab/show/proper+map">proper map</a></p> <p><a class="existingWikiWord" href="/nlab/show/sequentially+compact+topological+space">sequentially compact</a>, <a class="existingWikiWord" href="/nlab/show/countably+compact+topological+space">countably compact</a>, <a class="existingWikiWord" href="/nlab/show/locally+compact+topological+space">locally compact</a>, <a class="existingWikiWord" href="/nlab/show/sigma-compact+topological+space">sigma-compact</a>, <a class="existingWikiWord" href="/nlab/show/paracompact+space">paracompact</a>, <a class="existingWikiWord" href="/nlab/show/countably+paracompact+topological+space">countably paracompact</a>, <a class="existingWikiWord" href="/nlab/show/strongly+compact+topological+space">strongly compact</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compactly+generated+space">compactly generated space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/second-countable+space">second-countable space</a>, <a class="existingWikiWord" href="/nlab/show/first-countable+space">first-countable space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/contractible+space">contractible space</a>, <a class="existingWikiWord" href="/nlab/show/locally+contractible+space">locally contractible space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/connected+space">connected space</a>, <a class="existingWikiWord" href="/nlab/show/locally+connected+space">locally connected space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/simply-connected+space">simply-connected space</a>, <a class="existingWikiWord" href="/nlab/show/locally+simply-connected+space">locally simply-connected space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cell+complex">cell complex</a>, <a class="existingWikiWord" href="/nlab/show/CW-complex">CW-complex</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pointed+topological+space">pointed space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+vector+space">topological vector space</a>, <a class="existingWikiWord" href="/nlab/show/Banach+space">Banach space</a>, <a class="existingWikiWord" href="/nlab/show/Hilbert+space">Hilbert space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+group">topological group</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+vector+bundle">topological vector bundle</a>, <a class="existingWikiWord" href="/nlab/show/topological+K-theory">topological K-theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+manifold">topological manifold</a></p> </li> </ul> <p><strong>Examples</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/empty+space">empty space</a>, <a class="existingWikiWord" href="/nlab/show/point+space">point space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/discrete+space">discrete space</a>, <a class="existingWikiWord" href="/nlab/show/codiscrete+space">codiscrete space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Sierpinski+space">Sierpinski space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/order+topology">order topology</a>, <a class="existingWikiWord" href="/nlab/show/specialization+topology">specialization topology</a>, <a class="existingWikiWord" href="/nlab/show/Scott+topology">Scott topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Euclidean+space">Euclidean space</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/real+line">real line</a>, <a class="existingWikiWord" href="/nlab/show/plane">plane</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cylinder">cylinder</a>, <a class="existingWikiWord" href="/nlab/show/cone">cone</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sphere">sphere</a>, <a class="existingWikiWord" href="/nlab/show/ball">ball</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/circle">circle</a>, <a class="existingWikiWord" href="/nlab/show/torus">torus</a>, <a class="existingWikiWord" href="/nlab/show/annulus">annulus</a>, <a class="existingWikiWord" href="/nlab/show/Moebius+strip">Moebius strip</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/polytope">polytope</a>, <a class="existingWikiWord" href="/nlab/show/polyhedron">polyhedron</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/projective+space">projective space</a> (<a class="existingWikiWord" href="/nlab/show/real+projective+space">real</a>, <a class="existingWikiWord" href="/nlab/show/complex+projective+space">complex</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/classifying+space">classifying space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/configuration+space+%28mathematics%29">configuration space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/path">path</a>, <a class="existingWikiWord" href="/nlab/show/loop">loop</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+spaces">mapping spaces</a>: <a class="existingWikiWord" href="/nlab/show/compact-open+topology">compact-open topology</a>, <a class="existingWikiWord" href="/nlab/show/topology+of+uniform+convergence">topology of uniform convergence</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/loop+space">loop space</a>, <a class="existingWikiWord" href="/nlab/show/path+space">path space</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Zariski+topology">Zariski topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cantor+space">Cantor space</a>, <a class="existingWikiWord" href="/nlab/show/Mandelbrot+space">Mandelbrot space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Peano+curve">Peano curve</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/line+with+two+origins">line with two origins</a>, <a class="existingWikiWord" href="/nlab/show/long+line">long line</a>, <a class="existingWikiWord" href="/nlab/show/Sorgenfrey+line">Sorgenfrey line</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/K-topology">K-topology</a>, <a class="existingWikiWord" href="/nlab/show/Dowker+space">Dowker space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Warsaw+circle">Warsaw circle</a>, <a class="existingWikiWord" href="/nlab/show/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/Hausdorff+spaces+are+sober">Hausdorff spaces are sober</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/schemes+are+sober">schemes are sober</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/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/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/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/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/compact+spaces+equivalently+have+converging+subnet+of+every+net">compact spaces equivalently have converging subnet of every net</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Lebesgue+number+lemma">Lebesgue number lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/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/compact+spaces+equivalently+have+converging+subnet+of+every+net">compact spaces equivalently have converging subnet of every net</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/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/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/paracompact+Hausdorff+spaces+are+normal">paracompact Hausdorff spaces are normal</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/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/closed+injections+are+embeddings">closed injections are embeddings</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/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/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/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/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/second-countable+regular+spaces+are+paracompact">second-countable regular spaces are paracompact</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/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/Urysohn%27s+lemma">Urysohn's lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tietze+extension+theorem">Tietze extension theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tychonoff+theorem">Tychonoff theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/tube+lemma">tube lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Michael%27s+theorem">Michael's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Brouwer%27s+fixed+point+theorem">Brouwer's fixed point theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+invariance+of+dimension">topological invariance of dimension</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/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/Heine-Borel+theorem">Heine-Borel theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/intermediate+value+theorem">intermediate value theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/extreme+value+theorem">extreme value theorem</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/topological+homotopy+theory">topological homotopy theory</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/left+homotopy">left homotopy</a>, <a class="existingWikiWord" href="/nlab/show/right+homotopy">right homotopy</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+equivalence">homotopy equivalence</a>, <a class="existingWikiWord" href="/nlab/show/deformation+retract">deformation retract</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+group">fundamental group</a>, <a class="existingWikiWord" href="/nlab/show/covering+space">covering space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+theorem+of+covering+spaces">fundamental theorem of covering spaces</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+group">homotopy group</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weak+homotopy+equivalence">weak homotopy equivalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+theorem">Whitehead's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freudenthal+suspension+theorem">Freudenthal suspension theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/nerve+theorem">nerve theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+extension+property">homotopy extension property</a>, <a class="existingWikiWord" href="/nlab/show/Hurewicz+cofibration">Hurewicz cofibration</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+cofiber+sequence">cofiber sequence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Str%C3%B8m+model+category">Strøm model category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/classical+model+structure+on+topological+spaces">classical model structure on topological spaces</a></p> </li> </ul> </div></div> <h4 id="analysis">Analysis</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/analysis">analysis</a></strong> (<a class="existingWikiWord" href="/nlab/show/differential+calculus">differential</a>/<a class="existingWikiWord" href="/nlab/show/integral+calculus">integral</a> <a class="existingWikiWord" href="/nlab/show/calculus">calculus</a>, <a class="existingWikiWord" href="/nlab/show/functional+analysis">functional analysis</a>, <a class="existingWikiWord" href="/nlab/show/topology">topology</a>)</p> <p><a class="existingWikiWord" href="/nlab/show/epsilontic+analysis">epsilontic analysis</a></p> <p><a class="existingWikiWord" href="/nlab/show/infinitesimal+analysis">infinitesimal analysis</a></p> <p><a class="existingWikiWord" href="/nlab/show/computable+analysis">computable analysis</a></p> <p><em><a class="existingWikiWord" href="/nlab/show/Introduction+to+Topology+--+1">Introduction</a></em></p> <h2 id="basic_concepts">Basic concepts</h2> <p><a class="existingWikiWord" href="/nlab/show/triangle+inequality">triangle inequality</a></p> <p><a class="existingWikiWord" href="/nlab/show/metric+space">metric space</a>, <a class="existingWikiWord" href="/nlab/show/normed+vector+space">normed vector space</a></p> <p><a class="existingWikiWord" href="/nlab/show/open+ball">open ball</a>, <a class="existingWikiWord" href="/nlab/show/open+subset">open subset</a>, <a class="existingWikiWord" href="/nlab/show/neighbourhood">neighbourhood</a></p> <p><a class="existingWikiWord" href="/nlab/show/metric+topology">metric topology</a></p> <p><a class="existingWikiWord" href="/nlab/show/sequence">sequence</a>, <a class="existingWikiWord" href="/nlab/show/net">net</a></p> <p><a class="existingWikiWord" href="/nlab/show/convergence">convergence</a>, <a class="existingWikiWord" href="/nlab/show/limit+of+a+sequence">limit of a sequence</a></p> <p><a class="existingWikiWord" href="/nlab/show/compact+space">compactness</a>, <a class="existingWikiWord" href="/nlab/show/sequentially+compact+space">sequential compactness</a></p> <p><a class="existingWikiWord" href="/nlab/show/differentiation">differentiation</a>, <a class="existingWikiWord" href="/nlab/show/integration">integration</a></p> <p><a class="existingWikiWord" href="/nlab/show/topological+vector+space">topological vector space</a></p> <h2 id="basic_facts">Basic facts</h2> <p><a class="existingWikiWord" href="/nlab/show/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/intermediate+value+theorem">intermediate value theorem</a></p> <p><a class="existingWikiWord" href="/nlab/show/extreme+value+theorem">extreme value theorem</a></p> <p><a class="existingWikiWord" href="/nlab/show/Heine-Borel+theorem">Heine-Borel theorem</a></p> <p>…</p> </div></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></li> <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><a href='#properties'>Properties</a></li> <ul> <li><a href='#RelationToTopology'>Relation to topology</a></li> <li><a href='#LogicOfNets'>Logic of nets</a></li> </ul> <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/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/function">function</a> from a <a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/sequences">sequences</a>, for which <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/natural+numbers">natural numbers</a>. Regarded as a generalization of sequences, nets are used in <a class="existingWikiWord" href="/nlab/show/topology">topology</a> for formalization of the concept of <a class="existingWikiWord" href="/nlab/show/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/proper+filters">proper filters</a> (def. <a class="maruku-ref" href="#Filter"></a> below), their <em><a class="existingWikiWord" href="/nlab/show/eventuality+filters">eventuality filters</a></em> (def. <a class="maruku-ref" href="#EventualityFilter"></a> below).</p> <p>The concept of nets is motivated from the fact that where plain <a class="existingWikiWord" href="/nlab/show/sequences">sequences</a> detect <a class="existingWikiWord" href="/nlab/show/topology">topological</a> properties in <a class="existingWikiWord" href="/nlab/show/metric+spaces">metric spaces</a>, in generally they fail to do so in more general <a class="existingWikiWord" href="/nlab/show/topological+spaces">topological spaces</a>. For example <a class="existingWikiWord" href="/nlab/show/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/topological+spaces">topological spaces</a> being <a class="existingWikiWord" href="/nlab/show/sequentially+compact+space">sequentially compact</a> neither implies nor is implied by being <a class="existingWikiWord" href="/nlab/show/compact+space">compact</a> (see at <em><a class="existingWikiWord" href="/nlab/show/sequentially+compact+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/natural+numbers">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/directed+sets">directed sets</a> for nets in place of just the <a class="existingWikiWord" href="/nlab/show/natural+numbers">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"></a> below),</p> </li> <li> <p>the continuity of functions between them (prop. <a class="maruku-ref" href="#ContinuousFunctionsDetectedByNets"></a> below),</p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/Hausdorff+topological+space">Hausdorff</a> property (prop. <a class="maruku-ref" href="#NetsDetectHausdorff"></a> below),</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+topological+space">compactness</a> (prop. <a class="maruku-ref" href="#CompactSpacesEquivalentlyHaveConvergetSubnets"></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/filters">filters</a> of <a class="existingWikiWord" href="/nlab/show/subsets">subsets</a> which they eventually meet” (def. <a class="maruku-ref" href="#EventuallyAndFrequently"></a> below), called their <em><a class="existingWikiWord" href="/nlab/show/eventuality+filters">eventuality filters</a></em> (def. <a class="maruku-ref" href="#EventualityFilter"></a> below). For example equivalent filters are equal (in contrast to nets) and (unless in <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a>) the set of filters on a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/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/directed+set">directed set</a>)</strong></p> <p>A <em><a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a></em> is</p> <ul> <li>a <a class="existingWikiWord" href="/nlab/show/preordered+set">preordered set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/reflexive+relation">reflexive</a> and <a class="existingWikiWord" href="/nlab/show/transitive">transitive</a> <a class="existingWikiWord" href="/nlab/show/relation">relation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/finite+set">finite</a> <a class="existingWikiWord" href="/nlab/show/subset">subset</a> has an <a class="existingWikiWord" href="/nlab/show/upper+bound">upper bound</a>, hence for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/directed+set">directed set</a> of <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a>)</strong></p> <p>The <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math> with their canonical lower-or-equal relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> form a <a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a> (def. <a class="maruku-ref" href="#DirectedSet"></a>).</p> </div> <p>The key class of examples of nets, underlying their relation to <a class="existingWikiWord" href="/nlab/show/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/directed+set">directed set</a> of <a class="existingWikiWord" href="/nlab/show/neighbourhoods">neighbourhoods</a>)</strong></p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/topological+space">topological space</a> and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/neighbourhoods">neighbourhoods</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/directed+set">directed set</a> (def. <a class="maruku-ref" href="#DirectedSet"></a>).</p> </div> <div class="num_example" id="DirectedProductSet"> <h6 id="example_3">Example</h6> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>A</mi> <mo>≥</mo></msub></mrow><annotation encoding="application/x-tex">A_{\geq}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/directed+sets">directed sets</a> (def. <a class="maruku-ref" href="#DirectedSet"></a>). Then the <a class="existingWikiWord" href="/nlab/show/Cartesian+product">Cartesian product</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><mo>≔</mo><mspace width="thinmathspace"></mspace><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"></mspace><mtext>and</mtext><mspace width="thinmathspace"></mspace><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"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> a <a class="existingWikiWord" href="/nlab/show/set">set</a>, then a <em>net</em> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/directed+set">directed set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> (def. <a class="maruku-ref" href="#DirectedSet"></a>), called the <em>index set</em>,</p> </li> <li> <p>a <a class="existingWikiWord" href="/nlab/show/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>.</p> </li> </ol> <p>We say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/sequences">sequences</a> are <a class="existingWikiWord" href="/nlab/show/nets">nets</a>)</strong></p> <p>A <a class="existingWikiWord" href="/nlab/show/sequence">sequence</a> is a net (def. <a class="maruku-ref" href="#Net"></a>) whose directed set of indices is the <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>).</p> </div> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>Although the index set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> in def. <a class="maruku-ref" href="#Net"></a>, being a <a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a>, is equipped with a <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a>, the function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/partial+order">poset</a>.</p> <p>You can get around this if you instead define a net in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> as a <a class="existingWikiWord" href="/nlab/show/multi-valued+function">multi-valued function</a> from a partially ordered directed set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/sequence">sequence</a>. In some <a class="existingWikiWord" href="/nlab/show/type+theory">type-theoretic</a> <a class="existingWikiWord" href="/nlab/show/foundations">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/prefunction">prefunction</a>, like a function but not required to preserve <a class="existingWikiWord" href="/nlab/show/equality">equality</a>). On the other hand, every net with domain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/eventuality+filter">eventuality filter</a>) to a net with domain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>=</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a = b</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/eventually">eventually</a> and frequently)</strong></p> <p>Consider <a class="existingWikiWord" href="/nlab/show/net">net</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>), and given a <a class="existingWikiWord" href="/nlab/show/subset">subset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> is <em><a class="existingWikiWord" href="/nlab/show/eventually">eventually</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math></em> if there exists <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> is <em>frequently in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math></em> if for every index <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></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/convergence">convergence</a> of <a class="existingWikiWord" href="/nlab/show/nets">nets</a>)</strong></p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/topological+space">topological space</a>, and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/net">net</a> in the underlying set (def. <a class="maruku-ref" href="#Net"></a>).</p> <p>We say that the net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/convergence">converges</a></em> to an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/neighbourhood">neighbourhood</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> is eventually in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> (def. <a class="maruku-ref" href="#EventuallyAndFrequently"></a>); such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/limit+point">limit point</a></em> of the net;</p> </li> <li> <p><em>clusters</em> at <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/neighbourhood">neighbourhood</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> is frequently in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> (also def. <a class="maruku-ref" href="#EventuallyAndFrequently"></a>); such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/cluster+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/limit+points">limit points</a> of nets, according to def. <a class="maruku-ref" href="#Convergence"></a>, need not be unique. They are guaranteed to be unique in <a class="existingWikiWord" href="/nlab/show/Hausdorff+topological+spaces">Hausdorff spaces</a>, see prop. <a class="maruku-ref" href="#NetsDetectHausdorff"></a> below.</p> </div> <h3 id="subnets">Subnets</h3> <p>The definition of the concept of <em><a class="existingWikiWord" href="/nlab/show/sub-nets">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"></a> below becomes true, which states that <a class="existingWikiWord" href="/nlab/show/compact+spaces+equivalently+have+converging+subnet+of+every+net">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/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"></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"></a>, def. <a class="maruku-ref" href="#Kelley"></a>) are sufficient (in a sense made precise by theorem <a class="maruku-ref" href="#EquivalenceOfDefinitionsOfSubnets"></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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, and a net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, we say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is a <strong>subnet</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> maps <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> (that is, for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\beta \in B</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> is monotone (that is, for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> is cofinal (that is, for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, and a net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, we say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is a <strong>subnet</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> maps <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> (that is, for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>β</mi><mo>∈</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\beta \in B</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> is strongly cofinal (that is, for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> in definitions <a class="maruku-ref" href="#Willard"></a> and <a class="maruku-ref" href="#Kelley"></a> is <em>not</em> required to be an <a class="existingWikiWord" href="/nlab/show/injection">injection</a>, and it need not be. As a result, a <a class="existingWikiWord" href="/nlab/show/sequence">sequence</a> regarded as a <a class="existingWikiWord" href="/nlab/show/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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, and a net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, we say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is a <strong>subnet</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/eventuality+filter">eventuality filter</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> (def. <a class="maruku-ref" href="#EventualityFilter"></a>) refines the eventuality filter of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>. (Explicitly, for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is a (<a class="maruku-ref" href="#Willard"></a>)-subnet of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>)-subnet of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, using the same function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>.</li> <li>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is a (<a class="maruku-ref" href="#Kelley"></a>)-subnet of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>)-subnet of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>.</li> <li>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is a (<a class="maruku-ref" href="#AA"></a>)-subnet of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, then there is some net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</annotation></semantics></math> such that <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</annotation></semantics></math> is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> in the sense that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</annotation></semantics></math> are (<a class="maruku-ref" href="#AA"></a>)-subnets of each other, and</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</annotation></semantics></math> is a (<a class="maruku-ref" href="#Willard"></a>)-subnet of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>), there are enough (<a class="maruku-ref" href="#Willard"></a>)-subnets and (<a class="maruku-ref" href="#Kelley"></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/filter">filter</a>)</strong></p> <p>Given a <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> then a <a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/subsets">subsets</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/power+set">power set</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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/filter">filter</a></em> of subsets if it is closed under <a class="existingWikiWord" href="/nlab/show/intersections">intersections</a> and under taking supersets.</p> <p>The filter <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/inhabited+subset">inhabited</a>.</p> </div> <div class="num_defn" id="EventualityFilter"> <h6 id="definition_9">Definition</h6> <p><strong>(<a class="existingWikiWord" href="/nlab/show/eventuality+filter">eventuality filter</a>)</strong></p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> be a <a class="existingWikiWord" href="/nlab/show/set">set</a> and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> (def. <a class="maruku-ref" href="#Net"></a>).</p> <p>The <em><a class="existingWikiWord" href="/nlab/show/eventuality+filter">eventuality filter</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/filter">filter</a> (def. <a class="maruku-ref" href="#Filter"></a>) onsisting of the subsets that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><mo>⇔</mo><mspace width="thinmathspace"></mspace><mrow><mo>(</mo><mi>ν</mi><mspace width="thinmathspace"></mspace><mtext>is eventually in</mtext><mspace width="thinmathspace"></mspace><mi>U</mi><mo>)</mo></mrow><mspace width="thinmathspace"></mspace><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/eventuality+filter">eventuality filter</a> according to def. <a class="maruku-ref" href="#EventualityFilter"></a>. By def. <a class="maruku-ref" href="#AA"></a> and theorem <a class="maruku-ref" href="#EquivalenceOfDefinitionsOfSubnets"></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/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/filter">filter</a> is the <a class="existingWikiWord" href="/nlab/show/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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> be a <a class="existingWikiWord" href="/nlab/show/set">set</a> and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/filter">filter</a> of subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> (def. <a class="maruku-ref" href="#Filter"></a>). Ss Consider the <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/pairs">pairs</a> of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><mo>⇔</mo><mspace width="thinmathspace"></mspace><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"></mspace><mi>x</mi><mspace width="thinmathspace"></mspace><mtext>and</mtext><mspace width="thinmathspace"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/directed+set">directed set</a> according to def. <a class="maruku-ref" href="#DirectedSet"></a>. (It is actually enough to use only a base of the filters).</p> <p>Then the <em>filter net</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ν</mi> <mi>F</mi></msub></mrow><annotation encoding="application/x-tex">\nu_F</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℱ</mi></mrow><annotation encoding="application/x-tex">\mathcal{F}</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/net">net</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> (def. <a class="maruku-ref" href="#Net"></a>) given by</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><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/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> and a <a class="existingWikiWord" href="/nlab/show/filter">filter</a> of subsets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>), then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℱ</mi></mrow><annotation encoding="application/x-tex">\mathcal{F}</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/eventuality+filter">eventuality filter</a> (def. <a class="maruku-ref" href="#EventualityFilter"></a>) of its filter net (def. <a class="maruku-ref" href="#FilterNet"></a>).</p> </div> <p>For a related notion of filternet in a set X, see <a href="https://math.stackexchange.com/questions/1568548/where-has-this-common-generalization-of-nets-and-filters-been-written-down">this post</a></p> <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"></a> below),</p> </li> <li> <p>the continuity of functions between them (prop. <a class="maruku-ref" href="#ContinuousFunctionsDetectedByNets"></a> below),</p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/Hausdorff+topological+space">Hausdorff</a> property (prop. <a class="maruku-ref" href="#NetsDetectHausdorff"></a> below),</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+topological+space">compactness</a> (prop. <a class="maruku-ref" href="#CompactSpacesEquivalentlyHaveConvergetSubnets"></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/axiom+of+choice">axiom of choice</a> then:</p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/topological+space">topological space</a>. Then a <a class="existingWikiWord" href="/nlab/show/subset">subset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/open+subset">open</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> (is an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/complement">complement</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/closed+subset">closed subset</a> as seen not just by sequences but by nets, in that no <a class="existingWikiWord" href="/nlab/show/net">net</a> with elements in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>\</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">X\backslash S</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/converges">converges</a> to an element in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">x \in S</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/neighbourhood">neighbourhood</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>.</p> <p>For <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/directed+set">directed set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/open+neighbourhoods">open neighbourhoods</a> of this element (example <a class="maruku-ref" href="#DirectedSetOfNeighbourhods"></a>). Now the fact that the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/open+neighbourhood">open neighbourhood</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> intersects <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/axiom+of+choice">choose</a> elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> there exists <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/topological+space">topological space</a>. Then a <a class="existingWikiWord" href="/nlab/show/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/continuous+function">continuous</a> precisely if for every net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/convergence">converges</a> to some <a class="existingWikiWord" href="/nlab/show/limit+point">limit point</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>), the image net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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> </div> <div class="proof"> <h6 id="proof_2">Proof</h6> <p>In one direction, suppose that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/pre-image">pre-image</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, and so by the assumption that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> converges there is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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>Assuming <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>,</p> <p>Conversely, suppose that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> is not continuous. We need to find a net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> that converges to some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">x \in X</annotation></semantics></math>, and show that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∘</mo><mi>ν</mi></mrow><annotation encoding="application/x-tex">f \circ \nu</annotation></semantics></math> does not converge to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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>. (This is the <a class="existingWikiWord" href="/nlab/show/contrapositive">contrapositive</a> of the reverse implication, and by <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> equivalent to it.)</p> <p>Now that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a> this means that there exists a net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/closed+subset">closed subset</a> by the assumption that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a> this means that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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> <p><em>proof 2 (not using excluded middle)</em></p> <p>Assume for every net <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> is continuous.</p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> be a net with range contained in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> be a limit point of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math>. By <a class="maruku-ref" href="#TopologyDetectedByNets"></a>, it is sufficient to prove that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> converges to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>, since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> is open, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/convergence">convergence</a> relation that characterise whether it is topological (that is whether it comes from a topology on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/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/excluded+middle">excluded middle</a> and the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, then:</p> <p>A <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/Hausdorff+topological+space">Hausdorff topological space</a> precisely if no <a class="existingWikiWord" href="/nlab/show/net">net</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> (def. <a class="maruku-ref" href="#Net"></a>) converges to two distinct <a class="existingWikiWord" href="/nlab/show/limit+points">limit points</a> (def. <a class="maruku-ref" href="#Convergence"></a>).</p> </div> <div class="proof"> <h6 id="proof_3">Proof</h6> <p>In one direction, assume that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> which has limits points <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/proof+by+contradiction">proof by contradiction</a>.</p> <p>Conversely, assume that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/axiom+of+choice">choose</a> elements in these intersections</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>) and their directed Cartesian product set (example <a class="maruku-ref" href="#DirectedProductSet"></a>) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">x_1</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable displaystyle="true" columnalign="right left right left right left right left right left" columnspacing="0em"><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> <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> <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> <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"></mspace><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/compact+spaces+equivalently+have+converging+subnet+of+every+net">compact spaces are equivalently those for which every net has a converging subnet</a>)</strong></p> <p>Assuming <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> and the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, then:</p> <p>A <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/compact+topological+space">compact</a> precisely if every <a class="existingWikiWord" href="/nlab/show/net">net</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> (def. <a class="maruku-ref" href="#Net"></a>) has a <a class="existingWikiWord" href="/nlab/show/sub-net">sub-net</a> (def. <a class="maruku-ref" href="#Willard"></a>) that <a class="existingWikiWord" href="/nlab/show/convergence">converges</a> (def. <a class="maruku-ref" href="#Convergence"></a>).</p> </div> <p>We break up the <strong>proof</strong> into that of lemmas <a class="maruku-ref" href="#InACompactSpaceEveryNetHasAConvergentSubnet"></a> and <a class="maruku-ref" href="#IfEveryNetHasConvergentSubnetThenSpaceIsCompact"></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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/compact+topological+space">compact topological space</a>. Then every net in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/topological+closures">topological closures</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>S</mi> <mi>a</mi></msub><mspace width="thickmathspace"></mspace><mo>≔</mo><mspace width="thickmathspace"></mspace><mrow><mo>{</mo><msub><mi>ν</mi> <mi>b</mi></msub><mo>∈</mo><mi>X</mi><mspace width="thickmathspace"></mspace><mo stretchy="false">|</mo><mspace width="thickmathspace"></mspace><mi>b</mi><mo>≥</mo><mi>a</mi><mo>}</mo></mrow><mo>⊂</mo><mi>X</mi><mspace width="thinmathspace"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/finite+intersection+property">finite intersection property</a>, by the fact that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a>. Therefore <a href="finite+intersection+property#CompactnessInTermsOfFiniteIntersectionProperty">this prop.</a> implies from the assumption of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><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/neighbourhood">neighbourhood</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding="application/x-tex">U_x</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> intersects each of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/cluster+point">cluster point</a> (def <a class="maruku-ref" href="#Convergence"></a>) of the net.</p> <p>We will now produce a <a class="existingWikiWord" href="/nlab/show/sub-net">sub-net</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>B</mi></mtd> <mtd></mtd> <mtd><mover><mo>⟶</mo><mi>f</mi></mover></mtd> <mtd></mtd> <mtd><mi>A</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↘</mo></mtd> <mtd></mtd> <mtd><msub><mo>↙</mo> <mi>ν</mi></msub></mtd></mtr> <mtr><mtd></mtd> <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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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"></a>) of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> with the directed neighbourhood set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> (example <a class="maruku-ref" href="#DirectedSetOfNeighbourhods"></a>)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>B</mi><mspace width="thickmathspace"></mspace><mo>≔</mo><mspace width="thickmathspace"></mspace><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"></mspace><mo stretchy="false">|</mo><mspace width="thinmathspace"></mspace><msub><mi>ν</mi> <mi>a</mi></msub><mo>∈</mo><msub><mi>U</mi> <mi>X</mi></msub><mo>}</mo></mrow><mspace width="thinmathspace"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/preordered+set">preordered set</a>. We need to check that it is indeed directed, in that every pair of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>, hence that for every open neighbourhood <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding="application/x-tex">U_x</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> we may find <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> there exists some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi></mrow><annotation encoding="application/x-tex">a</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> implies that with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/excluded+middle">excluded middle</a>, then:</p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/topological+space">topological space</a>. If every <a class="existingWikiWord" href="/nlab/show/net">net</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/subnet">subnet</a> that <a class="existingWikiWord" href="/nlab/show/convergence">converges</a>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/compact+topological+space">compact topological space</a>.</p> </div> <div class="proof"> <h6 id="proof_5">Proof</h6> <p>By <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> we may equivalently prove the <a class="existingWikiWord" href="/nlab/show/contrapositive">contrapositive</a>: If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/excluded+middle">excluded middle</a>, then by <a href="finite+intersection+property#CompactnessInTermsOfFiniteIntersectionProperty">this prop.</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/closed+subsets">closed subsets</a> satisfying the <a class="existingWikiWord" href="/nlab/show/finite+intersection+property">finite intersection property</a>, but such that their intersection is empty: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/finite+set">finite</a> <a class="existingWikiWord" href="/nlab/show/subsets">subsets</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math>. By the assumption that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/finite+intersection+property">finite intersection property</a>, we may <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">choose</a> for each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/preordered+set">preordered set</a> under inclusion of subsets is clearly a <a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a>, with an upper bound of two finite subsets given by their <a class="existingWikiWord" href="/nlab/show/union">union</a>. Therefore we have defined a net</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>B</mi></mtd> <mtd></mtd> <mtd><mover><mo>⟶</mo><mi>f</mi></mover></mtd> <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> <mtd><mo>↘</mo></mtd> <mtd></mtd> <mtd><msub><mo>↙</mo> <mi>ν</mi></msub></mtd></mtr> <mtr><mtd></mtd> <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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/closed+subset">closed subset</a>, there would exist even an <a class="existingWikiWord" href="/nlab/show/open+neighbourhood">open neighbourhood</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>U</mi> <mi>x</mi></msub></mrow><annotation encoding="application/x-tex">U_x</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/proof+by+contradiction">proof by contradiction</a>.</p> </div> <h3 id="LogicOfNets">Logic of nets</h3> <p>A <a class="existingWikiWord" href="/nlab/show/property">property</a> of <a class="existingWikiWord" href="/nlab/show/elements">elements</a> of a <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/subset">subset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>.</p> <p>Being eventually in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>, def. <a class="maruku-ref" href="#EventuallyAndFrequently"></a>, is a weakening of being always in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/universal+quantifier">universal quantifier</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is a strengthening of being sometime in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/particular+quantifier">particular quantifier</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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/formal+logic">formal logic</a> out of these. Use <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is eventually true, and use <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mo>∀</mo> <mi>ν</mi></msub><mi>p</mi><mspace width="thickmathspace"></mspace><mo>⇒</mo><mspace width="thickmathspace"></mspace><mo lspace="0em" rspace="thinmathspace">ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mi>p</mi><mspace width="thickmathspace"></mspace><mo>⇒</mo><mspace width="thickmathspace"></mspace><mo lspace="0em" rspace="thinmathspace">ess</mo><msub><mo>∃</mo> <mi>ν</mi></msub><mi>p</mi><mspace width="thickmathspace"></mspace><mo>⇒</mo><mspace width="thickmathspace"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><mo>⇔</mo><mspace width="thickmathspace"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><mo>⇒</mo><mspace width="thickmathspace"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><mo>⇐</mo><mspace width="thickmathspace"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-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"></mspace><mo>⇔</mo><mspace width="thickmathspace"></mspace><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 xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo lspace="0em" rspace="thinmathspace">ess</mo><msub><mo>∀</mo> <mi>ν</mi></msub><mo>¬</mo><mi>p</mi><mspace width="thickmathspace"></mspace><mo>⇔</mo><mspace width="thickmathspace"></mspace><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/predicate+logic">predicate logic</a>. Note that the last item listed requires <a class="existingWikiWord" href="/nlab/show/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/almost+everywhere">almost everywhere</a>’ and its dual (‘not almost nowhere’ or ‘somewhere significant’) in <a class="existingWikiWord" href="/nlab/show/measure+spaces">measure spaces</a>.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sequential+net">sequential net</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/limit+of+a+net">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/Eric+Schechter">Eric Schechter</a>, sections 7.14–7.21 of <em><a class="existingWikiWord" href="/nlab/show/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/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> </body></html> </div> <div class="revisedby"> <p> Last revised on March 8, 2025 at 00:21:40. 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/net/39" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/net" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/net" accesskey="S" class="navlink" id="history" rel="nofollow">History (39 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>