\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{net}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{topology}{}\paragraph*{{Topology}}\label{topology}

[[!include topology - contents]]

\hypertarget{analysis}{}\paragraph*{{Analysis}}\label{analysis}

[[!include analysis - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{Idea}{Idea}\dotfill \pageref*{Idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{DirectedSets}{Directed sets}\dotfill \pageref*{DirectedSets} \linebreak
\noindent\hyperlink{Nets}{Nets}\dotfill \pageref*{Nets} \linebreak
\noindent\hyperlink{subnets}{Subnets}\dotfill \pageref*{subnets} \linebreak
\noindent\hyperlink{NetsAndFilters}{Eventuality filters}\dotfill \pageref*{NetsAndFilters} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{RelationToTopology}{Relation to topology}\dotfill \pageref*{RelationToTopology} \linebreak
\noindent\hyperlink{LogicOfNets}{Logic of nets}\dotfill \pageref*{LogicOfNets} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{Idea}{}\subsection*{{Idea}}\label{Idea}

A \emph{net} in a [[set]] $X$ is a [[function]] from a [[directed set]] $D$ to $X$. Special cases of nets are [[sequences]], for which $D = \mathbb{N}_{\leq}$ is the [[natural numbers]]. Regarded as a generalization of sequences, nets are used in [[topology]] for formalization of the concept of [[convergence]].

Nets are also called \emph{Moore--Smith sequences} and are equivalent (in a certain sense) to [[proper filters]] (def. \ref{Filter} below), their \emph{[[eventuality filters]]} (def. \ref{EventualityFilter} below).

The concept of nets is motivated from the fact that where plain [[sequences]] detect [[topology|topological]] properties in [[metric spaces]], in generally they fail to do so in more general [[topological spaces]]. For example [[sequentially compact metric spaces are equivalently compact metric spaces]], but for general [[topological spaces]] being [[sequentially compact space|sequentially compact]] neither implies nor is implied by being [[compact space|compact]] (see at \emph{[[sequentially compact space]]} \href{sequentially+compact+topological+space#Examples}{Examples and counter-examples}).

Inspection of these counter-examples reveals that the problem is that sequences indexed by the [[natural numbers]] 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 [[directed sets]] for nets in place of just the [[natural numbers]] for sequences fixes these two issues.

And indeed, as opposed to sequences, nets do detect

\begin{enumerate}%
\item the topology on general topological spaces (prop. \ref{TopologyDetectedByNets} below),


\item the continuity of functions between them (prop. \ref{ContinuousFunctionsDetectedByNets} below),


\item the [[Hausdorff topological space|Hausdorff]] property (prop. \ref{NetsDetectHausdorff} below),


\item [[compact topological space|compactness]] (prop. \ref{CompactSpacesEquivalentlyHaveConvergetSubnets} below).



\end{enumerate}
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 ``[[filters]] of [[subsets]] which they eventually meet'' (def. \ref{EventuallyAndFrequently} below), called their \emph{[[eventuality filters]]} (def. \ref{EventualityFilter} below). For example equivalent filters are equal (in contrast to nets) and (unless in [[predicative mathematics]]) the set of filters on a set $X$ is [[small set|small]] (not a proper class).

\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

\hypertarget{DirectedSets}{}\subsubsection*{{Directed sets}}\label{DirectedSets}

\begin{defn}
\label{DirectedSet}\hypertarget{DirectedSet}{}
\textbf{([[directed set]])}

A \emph{[[directed set]]} is

\begin{itemize}%
\item a [[preordered set]] $(D, \leq)$, hence a set $D$ equipped with a [[reflexive relation|reflexive]] and [[transitive]] [[relation]] $\leq$

\end{itemize}
such that

\begin{itemize}%
\item every [[finite set|finite]] [[subset]] has an [[upper bound]], hence for any $a,b \in D$ there exists $c \in D$ with $a \leq c$ and $b \leq c$.

\end{itemize}
\end{defn}
\begin{example}
\label{DirectedSetOfNaturalNumbers}\hypertarget{DirectedSetOfNaturalNumbers}{}
\textbf{([[directed set]] of [[natural numbers]])}

The [[natural numbers]] $\mathbb{N}$ with their canonical lower-or-equal relation $\leq$ form a [[directed set]] (def. \ref{DirectedSet}).

\end{example}
The key class of examples of nets, underlying their relation to [[topology]] (\hyperlink{RelationToTopology}{below}) is the following:

\begin{example}
\label{DirectedSetOfNeighbourhods}\hypertarget{DirectedSetOfNeighbourhods}{}
\textbf{([[directed set]] of [[neighbourhoods]])}

Let $(X, \tau)$ be a [[topological space]] and let $x \in X$ be an element of the underlying set. Then then set of $(Nbhd_X(x)_{\supset})$ [[neighbourhoods]] of $x$, ordered by \emph{reverse} inclusion, is a [[directed set]] (def. \ref{DirectedSet}).

\end{example}
\begin{example}
\label{DirectedProductSet}\hypertarget{DirectedProductSet}{}
Let $A_{\geq}$ and $B_{\geq}$ be two [[directed sets]] (def. \ref{DirectedSet}). Then the [[Cartesian product]] $A \times B$ of the underlying sets becomes itself a directed set by setting

\begin{displaymath}
\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)
  \,.
\end{displaymath}
\end{example}
\hypertarget{Nets}{}\subsubsection*{{Nets}}\label{Nets}

\begin{defn}
\label{Net}\hypertarget{Net}{}
For $X$ a [[set]], then a \emph{net} in $X$ is

\begin{enumerate}%
\item a [[directed set]] $A$ (def. \ref{DirectedSet}), called the \emph{index set},


\item a [[function]] $\nu \colon A \to X$ from (the underlying set of) $A$ to $X$.



\end{enumerate}
We say that $A$ \emph{indexes} the net.

\end{defn}
\begin{example}
\label{SequencesAreNets}\hypertarget{SequencesAreNets}{}
\textbf{([[sequences]] are [[nets]])}

A [[sequence]] is a net (def. \ref{Net}) whose directed set of indices is the [[natural numbers]] $(\mathbb{N}, \leq)$ (example \ref{DirectedSetOfNaturalNumbers}).

\end{example}
\begin{remark}
\label{}\hypertarget{}{}
Although the index set $A$ in def. \ref{Net}, being a [[directed set]], is equipped with a [[preorder]], the function $\nu \colon A \to X$ 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 [[partial order|poset]].

You can get around this if you instead define a net in $X$ as a [[multi-valued function]] from a partially ordered directed set $A$ to $X$. Although there is not much point to doing this in general, it can make a difference if you put restrictions on the possibilities for $A$, in particular if you consider the definition of [[sequence]]. In some [[type theory|type-theoretic]] [[foundations]] of mathematics, you can get the same effect by defining a net to be an `operation' (a [[prefunction]], like a function but not required to preserve [[equality]]). On the other hand, every net with domain $A$ is equivalent (in the sense of having the same [[eventuality filter]]) to a net with domain $A \times \mathbb{N}$, made into a partial order by defining $(a,m) \leq (b,n)$ iff $a = b$ and $m \leq n$ or $a \leq b$ and $m \lt n$.

\end{remark}
\begin{defn}
\label{EventuallyAndFrequently}\hypertarget{EventuallyAndFrequently}{}
\textbf{([[eventually]] and frequently)}

Consider [[net]] $\nu \colon A \to X$ (def. \ref{Net}), and given a [[subset]] $S \subset X$. We say that

\begin{enumerate}%
\item $\nu$ is \emph{[[eventually]] in $S$} if there exists $i \in A$ such that $\nu_j \in S$ for every $j \ge i$.


\item $\nu$ is \emph{frequently in $S$} if for every index $i \in A$, then $\nu_j \in S$ for some $j \ge i$.



\end{enumerate}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
Sometimes one says `infinitely often' in place of `frequently' in def. \ref{EventuallyAndFrequently} and even `cofinitely often' in place of `eventually'; these derive from the special case of sequences, where they may be taken literally.

\end{remark}
\begin{defn}
\label{Convergence}\hypertarget{Convergence}{}
\textbf{([[convergence]] of [[nets]])}

Let $(X,\tau)$ be a [[topological space]], and let $\nu \colon A \to X$ be a [[net]] in the underlying set (def. \ref{Net}).

We say that the net $\nu$

\begin{enumerate}%
\item \emph{[[convergence|converges]]} to an element $x \in X$ if given any [[neighbourhood]] $U$ of $x$, $\nu$ is eventually in $U$ (def. \ref{EventuallyAndFrequently}); such $x$ is called a \emph{[[limit point]]} of the net;


\item \emph{clusters} at $x$ if, for every [[neighbourhood]] $U$ of $x$, $\nu$ is frequently in $U$ (also def. \ref{EventuallyAndFrequently}); such $x$ is called a \emph{[[cluster point]]} of the net.



\end{enumerate}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
Beware that [[limit points]] of nets, according to def. \ref{Convergence}, need not be unique. They are guaranteed to be unique in [[Hausdorff topological spaces|Hausdorff spaces]], see prop. \ref{NetsDetectHausdorff} below.

\end{remark}
\hypertarget{subnets}{}\subsubsection*{{Subnets}}\label{subnets}

The definition of the concept of \emph{[[sub-nets]]} of a net requires some care. The point of the definition is to ensure that prop. \ref{CompactSpacesEquivalentlyHaveConvergetSubnets} below becomes true, which states that [[compact spaces equivalently have converging subnet of every net|compact spaces are equivalently those for which every net has a converging subnet]].

There are several different definitions of `[[subnet]]' 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 \ref{AA} which is correct in that it corresponds precisely to refinement of filters. However, the other two definitions (def. \ref{Willard}, def. \ref{Kelley}) are sufficient (in a sense made precise by theorem \ref{EquivalenceOfDefinitionsOfSubnets} below) and may be easier to work with.

\begin{defn}
\label{Willard}\hypertarget{Willard}{}
(Willard, 1970).

Given a net $(x_{\alpha})$ with index set $A$, and a net $(y_{\beta})$ with an index set $B$, we say that $y$ is a \textbf{subnet} of $x$ if:

We have a [[function]] $f\colon B \to A$ such that

\begin{itemize}%
\item $f$ maps $x$ to $y$ (that is, for every $\beta \in B$, $y_{\beta} = x_{f(\beta)}$);
\item $f$ is monotone (that is, for every $\beta_1 \geq \beta_2 \in B$, $f(\beta_1) \geq f(\beta_2)$);
\item $f$ is cofinal (that is, for every $\alpha \in A$ there is a $\beta \in B$ such that $f(\beta) \geq \alpha$).

\end{itemize}
\end{defn}
\begin{defn}
\label{Kelley}\hypertarget{Kelley}{}
(Kelley, 1955).

Given a net $(x_{\alpha})$ with index set $A$, and a net $(y_{\beta})$ with an index set $B$, we say that $y$ is a \textbf{subnet} of $x$ if:

We have a [[function]] $f\colon B \to A$ such that

\begin{itemize}%
\item $f$ maps $x$ to $y$ (that is, for every $\beta \in B$, $y_{\beta} = x_{f(\beta)}$);
\item $f$ is strongly cofinal (that is, for every $\alpha \in A$ there is a $\beta \in B$ such that, for every $\beta_1 \geq \beta \in B$, $f(\beta_1) \geq \alpha$).

\end{itemize}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
Notice that the function $f$ in definitions \ref{Willard} and \ref{Kelley} is \emph{not} required to be an [[injection]], and it need not be. As a result, a [[sequence]] regarded as a [[net]] in general has more sub-nets than it has sub-sequences.

\end{remark}
\begin{defn}
\label{AA}\hypertarget{AA}{}
(Smiley, 1957; \AA{}rnes \& Anden\ae{}s, 1972).

Given a net $(x_{\alpha})$ with index set $A$, and a net $(y_{\beta})$ with an index set $B$, we say that $y$ is a \textbf{subnet} of $x$ if:

The [[eventuality filter]] of $y$ (def. \ref{EventualityFilter}) refines the eventuality filter of $x$. (Explicitly, for every $\alpha \in A$ there is a $\beta \in B$ such that, for every $\beta_1 \geq \beta \in B$ there is an $\alpha_1 \geq \alpha \in A$ such that $y_{\beta_1} = x_{\alpha_1}$.)

\end{defn}
The equivalence between these definitions is as follows:

\begin{theorem}
\label{EquivalenceOfDefinitionsOfSubnets}\hypertarget{EquivalenceOfDefinitionsOfSubnets}{}
(\hyperlink{Schechter96}{Schechter, 1996}).

\begin{enumerate}%
\item If $y$ is a (\ref{Willard})-subnet of $x$, then $y$ is also a (\ref{Kelley})-subnet of $x$, using the same function $f$.
\item If $y$ is a (\ref{Kelley})-subnet of $x$, then $y$ is also a (\ref{AA})-subnet of $x$.
\item If $y$ is a (\ref{AA})-subnet of $x$, then there is some net $z$ such that\begin{itemize}%
\item $z$ is equivalent to $y$ in the sense that $y$ and $z$ are (\ref{AA})-subnets of each other, and
\item $z$ is a (\ref{Willard})-subnet of $x$, using some function.

\end{itemize}


\end{enumerate}
\end{theorem}
So from the perspective of definition (\ref{AA}), there are enough (\ref{Willard})-subnets and (\ref{Kelley})-subnets, up to equivalence.

\hypertarget{NetsAndFilters}{}\subsubsection*{{Eventuality filters}}\label{NetsAndFilters}

Recall that:

\begin{defn}
\label{Filter}\hypertarget{Filter}{}
\textbf{([[filter]])}

Given a [[set]] $X$ then a [[set]] of [[subsets]] of $X$, hence a subset of the [[power set]]

\begin{displaymath}
\mathcal{F} \subset P(X)
\end{displaymath}
is called a \emph{[[filter]]} of subsets if it is closed under [[intersections]] and under taking supersets.

The filter $\mathcal{F}$ is called \emph{proper} if each set in it is [[inhabited subset|inhabited]].

\end{defn}
\begin{defn}
\label{EventualityFilter}\hypertarget{EventualityFilter}{}
\textbf{([[eventuality filter]])}

Let $X$ be a [[set]] and let $\nu \colon D \to X$ be a net in $X$ (def. \ref{Net}).

The \emph{[[eventuality filter]]} $\mathcal{F}_\nu$ of the net $\nu$ is the [[filter]] (def. \ref{Filter}) onsisting of the subsets that $\nu$ is \emph{eventually in}, according to def. \ref{EventuallyAndFrequently}.

\begin{displaymath}
\left(
    (U \subset X) \in \mathcal{F}_\nu
  \right)
   \,\Leftrightarrow\,
  \left(
    \nu \, \text{is eventually in}\, U
  \right)
  \,.
\end{displaymath}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
\textbf{(equivalence of nets)}

Two nets are to be considered \textbf{equivalent} if they have the same [[eventuality filter]] according to def. \ref{EventualityFilter}. By def. \ref{AA} and theorem \ref{EquivalenceOfDefinitionsOfSubnets}, this means equivalently that they are both subnets of each other.

In particular, equivalent nets define the same logical quantifiers (see \hyperlink{LogicOfNets}{below}) and are therefore indeed equivalent for the application to [[topology]] (see \hyperlink{RelationToTopology}{below}).

(Of course, it is possible to distinguish them by using the standard logical quantifiers instead.)

\end{remark}
Conversely, every [[filter]] is the [[eventuality filter]] of some net:

\begin{defn}
\label{FilterNet}\hypertarget{FilterNet}{}
\textbf{(nets from filters)}

Let $X$ be a [[set]] and let $\mathcal{F} \subset P(X)$ be a [[filter]] of subsets of $X$ (def. \ref{Filter}). Ss Consider the [[disjoint union]] $\underset{U \in \mathcal{F}}{\sqcup}$ of subsets in $\mathcal{F}$, hence the set whose elements are [[pairs]] of the form $(U,x)$, where $x \in U \in \mathcal{F}$. Equipped with the ordering

\begin{displaymath}
\left(
    (U,x) \geq (V,y)  
  \right) 
  \,\Leftrightarrow\,
  \left(
    U \subset V
  \right)
  \phantom{AAA}
  \text{regardless of}\, x\, \text{and} \, y
\end{displaymath}
the fact that $\mathcal{F}$ is a proper filter implies that this is a [[directed set]] according to def. \ref{DirectedSet}. (It is actually enough to use only a base of the filters).

Then the \emph{filter net} $\nu_F$ of $\mathcal{F}$ is the [[net]] on $X$ (def. \ref{Net}) given by

\begin{displaymath}
\itexarray{
    \left(
      \underset{U \in \mathcal{F}}{\sqcup} U
    \right)_{\supset}
      &\overset{\nu_{\mathcal{F}}}{\longrightarrow}&
    X
    \\
    (U,x) &\overset{\phantom{AAA}}{\mapsto}& x
  }
  \,.
\end{displaymath}
\end{defn}
\begin{prop}
\label{}\hypertarget{}{}
Given a [[set]] $X$ and a [[filter]] of subsets $\mathcal{F} \subset P(X)$ (def. \ref{Filter}), then $\mathcal{F}$ is the [[eventuality filter]] (def. \ref{EventualityFilter}) of its filter net (def. \ref{FilterNet}).

\end{prop}
\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{RelationToTopology}{}\subsubsection*{{Relation to topology}}\label{RelationToTopology}

We discuss that nets detect:

\begin{enumerate}%
\item the topology on general topological spaces (prop. \ref{TopologyDetectedByNets} below),


\item the continuity of functions between them (prop. \ref{ContinuousFunctionsDetectedByNets} below),


\item the [[Hausdorff topological space|Hausdorff]] property (prop. \ref{NetsDetectHausdorff} below),


\item [[compact topological space|compactness]] (prop. \ref{CompactSpacesEquivalentlyHaveConvergetSubnets} below).



\end{enumerate}
\begin{prop}
\label{TopologyDetectedByNets}\hypertarget{TopologyDetectedByNets}{}
\textbf{(topology detected by nets)}

Using the [[axiom of choice]] then:

Let $(X, \tau)$ be a [[topological space]]. Then a [[subset]] $(U \subset X)$ is [[open subset|open]] in $X$ (is an element of $\tau \subset P(X)$) precisely if its [[complement]] $X \backslash S$ is a [[closed subset]] as seen not just by sequences but by nets, in that no [[net]] with elements in $X\backslash S$, $\nu \colon A \to X\backslash S \hookrightarrow X$, [[converges]] to an element in $S$.

\end{prop}
\begin{proof}
In one direction, let $S \subset X$ be open, and consider a net $\nu \colon A \to X \backslash S \subset X$. We need to show that for every point $x \in S$, $x$ is not a limiting point of the net.

But by assumption then $S$ is a [[neighbourhood]] of $x$ which does not contain any element of the net, and so by definition of convergence it is not a limit of this net.

Conversely, let $S \subset X$ be a subset that is not open. We need to show that then there exists a net $\nu \colon A \to X\backslash S \subset X$ that converges to a point in $S$.

For $x \in X$, consider the [[directed set]] $Nbhd_X(x)_{\supset}$ of [[open neighbourhoods]] of this element (example \ref{DirectedSetOfNeighbourhods}). Now the fact that the set $S$ is not open means that there exists an element $s \in S \subset X$ such that every [[open neighbourhood]] $U$ of $s$ intersects $X \backslash S$. This means that we may [[axiom of choice|choose]] elements $x_U \in U \cap (X \backslash S)$, and hence define a net

\begin{displaymath}
\itexarray{
    Nbhds_X(s) &\overset{\nu}{\longrightarrow}& X \backslash S  \subset X
    \\
    U &\mapsto& x_U
  }
  \,.
\end{displaymath}
But by construction this net has the property that for every neighbourhood $V$ of $s$ there exists $U \in Nbhd_X(s)$ such that for all $U' \subset U$ then $x_{U'} \in V$, namely $U = V$. Hence the net converges to $s$.

\end{proof}
\begin{prop}
\label{ContinuousFunctionsDetectedByNets}\hypertarget{ContinuousFunctionsDetectedByNets}{}
\textbf{(continuous functions detected by nets)}

Assuming [[excluded middle]], then

Let $(X,\tau_X)$ and $(Y,\tau_Y)$ be two [[topological space]]. Then a [[function]] $f \colon X \to Y$ between their underlying sets is [[continuous function|continuous]] precisely if for every net $\nu \colon A \to X$ that [[convergence|converges]] to some [[limit point]] $x \in X$ (def. \ref{Convergence}), the image net $f\circ \nu$ converges to $f(x)\in Y$.

\end{prop}
\begin{proof}
In one direction, suppose that $f \colon X \to Y$ is continuous, and that $\nu \colon A \to X$ converges to some $x \in X$. We need to show that $f \circ \nu$ converges to $f(x) \in Y$, hence that for every neighbourhood $U_{f(x)} \subset Y$ there exists $i \in A$ such that $f(\nu(j)) \in U_{f(x)}$ for all $j \geq i$.

But since $f$ is continuous, the [[pre-image]] $f^{-1}(U_{f(x)}) \subset X$ is an open neighbourhood of $x$, and so by the assumption that $\nu$ converges there is an $i \in A$ such that $\nu(j) \in f^{-1}(U_{f(x)})$ for all $j \geq i$. By applying $f$, this is the required statement.

Conversely, suppose that $f$ is not continuous, and that the net $\nu$ converges to some $x \in X$. We need to show that then $f \circ \nu$ does not converge to $f(x)$. (This is the [[contrapositive]] of the reverse implication, and by [[excluded middle]] equivalent to it.)

Now that $f$ is not continuous means that there exists an open subset $U \subset Y$ such that the pre-image $f^{-1}(U)$ is not open. By prop. \ref{TopologyDetectedByNets} this means that there exists a net $\nu$ in $X \backslash f^{-1}(U)$ that converges to an element $x \in f^{-1}(U)$. But this means that $f \circ \nu$ is a net in the $Y \backslash U$, which is a [[closed subset]] by the assumption that $U$ is open. Again by prop. \ref{TopologyDetectedByNets} this means that $f\circ \nu$ converges to an element in $Y \backslash U$, and hence not to $f(x) \in U$.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
It is possible to define elementary conditions on this [[convergence]] relation that characterise whether it is topological (that is whether it comes from a topology on $X$), although these are a bit complicated.

By keeping only the simple conditions, one gets the definition of a [[convergence space]]; 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).

\end{remark}
\begin{prop}
\label{NetsDetectHausdorff}\hypertarget{NetsDetectHausdorff}{}
\textbf{(Hausdorff property detected by nets)}

Assuming [[excluded middle]] and the [[axiom of choice]], then:

A [[topological space]] $(X,\tau)$ is [[Hausdorff topological space]] precisely if no [[net]] in $X$ (def. \ref{Net}) converges to two distinct [[limit points]] (def. \ref{Convergence}).

\end{prop}
\begin{proof}
In one direction, assume that $(X,\tau)$ is a Hausdorff space, and that $\nu \colon A \to X$ is a net in $X$ which has limits points $x_1, x_2 \in X$. We need to show that then $x_1 = x_2$.

Assume on the contrary that the two points were different, $x_1 \neq x_2$. By assumption of Hausdorffness, these would then have disjoint open neighbourhoods $U_{x_1}, U_{x_2}$, i.e. $U_1 \cap U_2 = \emptyset$. By definition of convergence, there would thus be $a_1, a_2 \in A$ such that $\nu_{a_1 \leq \bullet} \in U_{x_1}$ and $\nu_{a_2 \leq \bullet} \in U_{x_2}$. Moreover, by the definition of directed set, this would imply $a_3 \in A$ with $a_1, a_2 \leq a_3$, and hence that $x_{a_3 \leq \bullet} \in U_{x_1} \cap U_{x_2}$. This is in contradiction to the emptiness of the intersection, and hence we have a [[proof by contradiction]].

Conversely, assume that $(X,\tau)$ is not a Hausdorff space. We need to show that then there exists a net $\nu$ in $X$ with two distinct limit points.

That $(X,\tau)$ is not Hausdorff means that there are two distinct points $x_1, x_2 \in X$ such that every open neighbourhood of $x_1$ intersects every open neighbourhood of $x_2$. Hence we may [[axiom of choice|choose]] elements in these intersections

\begin{displaymath}
x_{U_{x_1}, U_{x_2}} \in U_{x_1}, U_{x_2}
  \,.
\end{displaymath}
Consider the directed neighbourhood sets $Nbhd_X(x_1)_{\supset}$ and $Nbhd_X(x_2)_{\supset}$ of these two points (example \ref{DirectedSetOfNeighbourhods}) and their directed Cartesian product set (example \ref{DirectedProductSet}) $Nbhd_X(x_1)_{\supset} \times Nbhd_X(x_2)_{\supset}$. The above elements then define a net

\begin{displaymath}
\itexarray{
     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}
  }
  \,.
\end{displaymath}
We conclude by claiming that $x_1$ and $x_2$ are both limit points of this net. We show this for $x_1$, the argument for $x_2$ is directly analogous:

Let $U_{x_1}$ be an open neighbourhood of $x_1$. We need to find an element $(V_1, V_2) \in Nbhd_X(x_1) \times Nbhd_X(x_2)$ such that for all $(W_1, W_2) \subset (V_1, V_2)$ then $\nu_{(W_1, W_2)} \in U_{x_1}$.

Take $V_1 \coloneqq U_{x_1}$ and take $V_2 = X$. Then by construction

\begin{displaymath}
\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}
  \,.
\end{displaymath}
\end{proof}
\begin{prop}
\label{CompactSpacesEquivalentlyHaveConvergetSubnets}\hypertarget{CompactSpacesEquivalentlyHaveConvergetSubnets}{}
\textbf{([[compact spaces equivalently have converging subnet of every net|compact spaces are equivalently those for which every net has a converging subnet]])}

Assuming [[excluded middle]] and the [[axiom of choice]], then:

A [[topological space]] $(X,\tau)$ is [[compact topological space|compact]] precisely if every [[net]] in $X$ (def. \ref{Net}) has a [[sub-net]] (def. \ref{Willard}) that [[convergence|converges]] (def. \ref{Convergence}).

\end{prop}
We break up the \textbf{proof} into that of lemmas \ref{InACompactSpaceEveryNetHasAConvergentSubnet} and \ref{IfEveryNetHasConvergentSubnetThenSpaceIsCompact}:

\begin{example}
\label{InACompactSpaceEveryNetHasAConvergentSubnet}\hypertarget{InACompactSpaceEveryNetHasAConvergentSubnet}{}
\textbf{(in a compact space, every net has a convergent subnet)}

Let $(X,\tau)$ be a [[compact topological space]]. Then every net in $X$ has a convergent subnet.

\end{example}
\begin{proof}
Let $\nu \colon A \to X$ be a net. We need to show that there is a subnet which converges.

For $a \in A$ consider the [[topological closures]] $Cl(S_a)$ of the sets $S_a$ of elements of the net beyond some fixed index:

\begin{displaymath}
S_a 
    \;\coloneqq\;
  \left\{
    \nu_b  \in X \;\vert\; b \geq a
  \right\}
  \subset X
  \,.
\end{displaymath}
Observe that the set $\{S_a \subset X\}_{a \in A}$ and hence also the set $\{Cl(S_a) \subset X\}_{a \in A}$ has the [[finite intersection property]], by the fact that $A$ is a [[directed set]]. Therefore \href{finite+intersection+property#CompactnessInTermsOfFiniteIntersectionProperty}{this prop.} implies from the assumption of $X$ being compact that the intersection of \emph{all} the $Cl(S_a)$ is non-empty, hence that there is an element

\begin{displaymath}
x \in \underset{a \in A}{\cap}  Cl(S_a)
  \,.
\end{displaymath}
In particular every [[neighbourhood]] $U_x$ of $x$ intersects each of the $Cl(S_a)$, and hence also each of the $S_a$. By definition of the $S_a$, this means that for every $a \in A$ there exists $b \geq a$ such that $\nu_b \in U_x$, hence that $x$ is a [[cluster point]] (def \ref{Convergence}) of the net.

We will now produce a [[sub-net]]

\begin{displaymath}
\itexarray{
     B && \overset{f}{\longrightarrow} && A
     \\
     & \searrow && \swarrow_{\nu}
     \\
     && X
  }
\end{displaymath}
that converges to this cluster point. To this end, we first need to build the domain directed set $B$. Take it to be the sub-directed set of the Cartesian product directed set (example \ref{DirectedProductSet}) of $A$ with the directed neighbourhood set $Nbhd_X(x)$ of $x$ (example \ref{DirectedSetOfNeighbourhods})

\begin{displaymath}
B \subset A_{\leq} \times Nbhd_X(x)_{\supset}
\end{displaymath}
on those pairs such that the element of the net indexed by the first component is contained in the second component:

\begin{displaymath}
B 
    \;\coloneqq\;
  \left\{
     (a,U_x)  \,\vert \, \nu_a \in U_X
  \right\}
  \,.
\end{displaymath}
It is clear $B$ is a [[preordered set]]. We need to check that it is indeed directed, in that every pair of elements $(a_1, U_1)$, $(a_2, U_2)$ has a common upper bound $(a_{bd}, U_{bd})$. Now since $A$ itself is directed, there is an upper bound $a_3 \geq a_1, a_2$, and since $x$ is a cluster point of the net there is moreover an $a_{bd} \geq a_3 \geq a_1, a_3$ such that $\nu_{a_{bd}} \in U_1 \cap U_2$. Hence with $U_{bd} \coloneqq U_1 \cap U_2$ we have obtained the required pair.

Next take the function $f$ to be given by

\begin{displaymath}
\itexarray{
     B &\overset{f}{\longrightarrow}& A
     \\
     (a, U) &\overset{\phantom{AAA}}{\mapsto}& a
  }
  \,.
\end{displaymath}
This is clearly order preserving, and it is cofinal since it is even a surjection. Hence we have defined a subnet $\nu \circ f$.

It now remains to see that $\nu \circ f$ converges to $x$, hence that for every open neighbourhood $U_x$ of $x$ we may find $(a,U)$ such that for all $(b,V)$ with $a \leq b$ and $U \supset V$ then $\nu(f(b,V)) = \nu(b) \in U_x$. Now by the nature of $x$ there exists some $a$ with $\nu_a \in U_x$, and hence if we take $U \coloneqq U_x$ then nature of $B$ implies that with $(b, V) \geq (a,U_x)$ then $b \in V \subset U_x$.

\end{proof}
\begin{example}
\label{IfEveryNetHasConvergentSubnetThenSpaceIsCompact}\hypertarget{IfEveryNetHasConvergentSubnetThenSpaceIsCompact}{}
Assuming [[excluded middle]], then:

Let $(X,\tau)$ be a [[topological space]]. If every [[net]] in $X$ has a [[subnet]] that [[convergence|converges]], then $(X,\tau)$ is a [[compact topological space]].

\end{example}
\begin{proof}
By [[excluded middle]] we may equivalently prove the [[contrapositive]]: If $(X,\tau)$ is not compact, then not every net in $X$ has a convergent subnet.

Hence assume that $(X,\tau)$ is not compact. We need to produce a net without a convergent subnet.

Again by [[excluded middle]], then by \href{finite+intersection+property#CompactnessInTermsOfFiniteIntersectionProperty}{this prop.} $(X,\tau)$ not being compact means equivalently that there exists a set $\{C_i \subset X\}_{i \in I}$ of [[closed subsets]] satisfying the [[finite intersection property]], but such that their intersection is empty: $\underset{i \in I}{\cap} C_i = \emptyset$.

Consider then $P_{fin}(I)$, the set of [[finite set|finite]] [[subsets]] of $I$. By the assumption that $\{C_i \subset X\}_{i \in I}$ satisfies the [[finite intersection property]], we may [[axiom of choice|choose]] for each $J \in P_{fin}(I)$ an element

\begin{displaymath}
x_J \in \underset{i \in J \subset I}{\cap} C_i
  \,.
\end{displaymath}
Now $P_{fin}(X)$ regarded as a [[preordered set]] under inclusion of subsets is clearly a [[directed set]], with an upper bound of two finite subsets given by their [[union]]. Therefore we have defined a net

\begin{displaymath}
\itexarray{
     P_{fin}(X)_{\subset} &\overset{\nu}{\longrightarrow}& X
     \\
     J &\overset{\phantom{AAA}}{\mapsto}& x_J
  }
  \,.
\end{displaymath}
We will show that this net has no converging subnet.

Assume on the contrary that there were a subnet

\begin{displaymath}
\itexarray{
     B && \overset{f}{\longrightarrow} && P_{fin}(X)
     \\
     & \searrow && \swarrow_{\nu}
     \\
     && X
  }
\end{displaymath}
which converges to some $x \in X$.

By the assumption that $\underset{i \in I}{\cap} C_i = \emptyset$, there would exist an $i_x \in I$ such that $x \neq C_{i_x}$, and because $C_i$ is a [[closed subset]], there would exist even an [[open neighbourhood]] $U_x$ of $x$ such that $U_x \cap C_{i_x} = \emptyset$. This would imply that $x_J \neq U_x$ for all $J \supset \{i_x\}$.

Now since the function $f$ defining the subset is cofinal, there would exist $b_1 \in B$ such that $\{i_x\} \subset f(b_1)$. Moreover, by the assumption that the subnet converges, there would also be $b_2 \in B$ such that $\nu_{b_2 \leq \bullet} \in U_x$. Since $B$ is directed, there would then be an upper bound $b \geq b_1, b_2$ of these two elements. This hence satisfies both $\nu_{f(e)} \in U_x$ as well as $\{i_x\} \subset f(b_1) \subset f(b)$. But the latter of these two means that $\nu_{f(b)}$ is not in $U_x$, which is a contradiction to the former. Thus we have a [[proof by contradiction]].

\end{proof}
\hypertarget{LogicOfNets}{}\subsubsection*{{Logic of nets}}\label{LogicOfNets}

A [[property]] of [[elements]] of a [[set]] $X$ (given by the [[subset]] $S \subset X$ of those elements of $X$ satisfying this property) may be applied to nets in $X$.

Being eventually in $S$, def. \ref{EventuallyAndFrequently}, is a weakening of being always in $S$ (given by the [[universal quantifier]] $\forall_\nu$), while being frequently in $S$ is a strengthening of being sometime in $S$ (given by the [[particular quantifier]] $\exists_\nu$). Indeed we can build a [[formal logic]] out of these. Use $\ess\forall i, p[\nu_i]$ or $\ess\forall_\nu p$ to mean that a predicate $p$ in $X$ is eventually true, and use $\ess\exists i, p[\nu_i]$ or $\ess\exists_\nu p$ to mean that $p$ is frequently true. Then we have:

\begin{displaymath}
\forall_\nu p \;\Rightarrow\; \ess\forall_\nu p \;\Rightarrow\; \ess\exists_\nu p \;\Rightarrow\; \exists_\nu p
\end{displaymath}
\begin{displaymath}
\ess\forall_\nu (p \wedge q) \;\Leftrightarrow\; \ess\forall_\nu p \wedge \ess\forall_\nu q
\end{displaymath}
\begin{displaymath}
\ess\exists_\nu (p \wedge q) \;\Rightarrow\; \ess\exists_\nu p \wedge \ess\exists_\nu q
\end{displaymath}
\begin{displaymath}
\ess\forall_\nu (p \vee q) \;\Leftarrow\; \ess\forall_\nu p \wedge \ess\forall_\nu q
\end{displaymath}
\begin{displaymath}
\ess\exists_\nu (p \vee q) \;\Leftrightarrow\; \ess\exists_\nu p \vee \ess\exists_\nu q
\end{displaymath}
\begin{displaymath}
\ess\forall_\nu \neg{p} \;\Leftrightarrow\; \neg\ess\exists_\nu p
\end{displaymath}
and other analogues of theorems from [[predicate logic]]. Note that the last item listed requires [[excluded middle]] even though its analogue from ordinary predicate logic does not.

A similar logic is satisfied by `[[almost everywhere]]' and its dual (`not almost nowhere' or `somewhere significant') in [[measure spaces]].

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[limit of a net]]


\item \href{Tychonoff+theorem#ProofViaNets}{Tychonoff theorem -- Proof via net convergence}



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

A textbook account is in

\begin{itemize}%
\item [[Eric Schechter]], sections 7.14--7.21 of \emph{[[Handbook of Analysis and its Foundations]]}, Academic Press (1996)

\end{itemize}
Lecture notes include

\begin{itemize}%
\item [[Stijn Vermeeren]], \emph{Sequences and nets in topology}, 2010 (\href{http://stijnvermeeren.be/download/mathematics/nets.pdf}{pdf})

\end{itemize}
[[!redirects net]] [[!redirects nets]]



\end{document}