> [!definition]
>
> Let $X$ be a [[Set|set]] and $A$ be a [[Directed Set|directed set]]. A **net** in $X$ is a [[Function|mapping]] from $A$ to $X$, denoted as $\net{x}$.
> [!definition]
>
> A net $\net{x}$ is **eventually** in $E \subset X$ if there exists $\alpha \in A$ such that $x_{\beta} \in E$ for all $\beta \gtrsim \alpha$.
> [!definition]
>
> A net $\net{x}$ is **frequently** in $E \subset X$ if for all $\alpha \in A$ there exists $\beta \gtrsim \alpha$ such that $x_{\beta} \in E$.
> [!definition]
>
> Let $(X, \topo)$ be a [[Topological Space|topological space]] and $A$ be a directed set. A net $\net{x}$ [[Limit|converges]] to $x \in X$ if $\net{x}$ is eventually in $U$ for any [[Neighbourhood|neighbourhood]] $U$ of $x$.
> [!definition]
>
> Let $X$ be a [[Topological Vector Space|topological vector space]] and $\net{x}$ be a net in $X$. $\net{x}$ is **Cauchy** if the net $\angles{x_\alpha - x_\beta}_{(\alpha, \beta) \in A^2}$ converges to $0$.
> [!definition]
>
> Let $(X, \topo)$ be a topological space and $A$ be a directed set. A point $x \in X$ is a **cluster point** of $\net{x}$ if $\net{x}$ is frequently in $U$ for any neighbourhood $U$ of $x$.
> [!quote] Idea
>
> Like a subsequence, a subnet is a collection of points in the original net structured in a way that maintains the "direction forward". The second condition does the same thing as the requirement for subsequence indices to be strictly increasing.
> [!definition]
>
> Let $\net{x}$ be a net. A **subnet** $\angles{y_\beta}_{\beta \in B}$ is a net with a map $\beta \mapsto \alpha_\beta$ such that
> - $y_\beta = x_{\alpha_\beta}$
> - For every $\alpha_0 \in A$ there exists a $\beta_0 \in B$ such that $\alpha_\beta \gtrsim \alpha_0$ whenever $\beta \gtrsim \beta_0$.
> [!theorem]
>
> Let $(X, \topo)$ be a topological space and $\net{x}$ be a net. Then $x \in X$ is a cluster point of $\angles{x_\alpha}$ if and only if there exists a subnet $\angles{y_\beta}$ such that $y_\beta \to x$.
>
> *Proof*. Suppose that $x \in X$ is a cluster point of $\angles{x_\alpha}$, then $\angles{x_\alpha}$ is frequently in $U$ for any $U \in \cn(x)$.
>
> Let $B = \cn(x) \times A$ be a directed set, and for every $(U, \gamma) \in B$, let $\alpha_{(U, \gamma)}$ be such that $x_{\alpha_{(U, \gamma)}} \in U$ and $\alpha_{(U, \gamma)} \gtrsim \gamma$ (since $\angles{x_\alpha}$ is frequently in $B$). Then for every $\gamma_0 \in A$, we can find $(U, \gamma_0)$ in $\beta$ such that $\alpha_{(V, \gamma)} \gtrsim \alpha_{(U, \gamma_0)} \gtrsim \gamma_0$ for all $(V, \gamma) \gtrsim (U, \gamma_0)$, and $\angles{x_{\alpha_{(U, \gamma)}}}$ is a subnet of $\angles{x_\alpha}$.
>
> For any neighbourhood $U \in \cn(x)$, we can find $(U, \gamma_0) \in \beta$ such that $x_{\alpha_{(V, \gamma)}} \in U$ for all $(V, \gamma) \gtrsim (U, \gamma_0)$. Therefore $x_{\alpha_{(U, \gamma)}} \to x$.
>
> Now suppose that there exists a subnet $\angles{y_\beta}$ such that $y_\beta \to x$. Then for any $\alpha_0 \in A$, we can find $\beta_0 \in B$ such that $\alpha_\beta \gtrsim \alpha_0$ for all $\beta \gtrsim \beta_0$. Let $U \in \cn(x)$, then since $y_\beta \to x$, there exists $\beta \in B$ such that $y_\gamma \in U$ for all $\gamma \gtrsim \beta$. Let $\gamma$ be such that $\gamma \gtrsim \beta_0$ and $\gamma \gtrsim \beta$, then $\alpha_\gamma \gtrsim \alpha_0$ and $y_\gamma = x_{\alpha_\gamma} \in U$. Therefore $\angles{x_\alpha}$ is frequently in $U$, and $x$ is a cluster point of $\angles{x_\alpha}$.