[proofplan] Part 1 (nets to filters): we verify the filter axioms for $\mathcal{F}_s$, then show that convergence and clustering of the net translate directly into convergence and clustering of $\mathcal{F}_s$, using the equivalence between "eventually in $A$" and "$A \in \mathcal{F}_s$." Part 2 (filters to nets): we verify that $D_\mathcal{F}$ is directed, then show convergence and clustering equivalences by unwinding the definitions through the canonical net's construction. [/proofplan]

## Part 1: From nets to filters

[step:Verify that $\mathcal{F}_s$ is a filter on $X$] Let $(s_\alpha)_{\alpha \in D}$ be a net in $X$. The eventuality filter is \begin{align*} \mathcal{F}_s := \{A \subset X : \text{there exists } \alpha_0 \in D \text{ such that } s_\alpha \in A \text{ for all } \alpha \succeq \alpha_0\}. \end{align*} We verify the three filter axioms. **Non-degeneracy:** $\varnothing \notin \mathcal{F}_s$, since no $s_\alpha$ can belong to $\varnothing$. Also, $X \in \mathcal{F}_s$, since $s_\alpha \in X$ for all $\alpha$. **Closure under finite intersections:** If $A, B \in \mathcal{F}_s$, then there exist $\alpha_1, \alpha_2 \in D$ with $s_\alpha \in A$ for $\alpha \succeq \alpha_1$ and $s_\alpha \in B$ for $\alpha \succeq \alpha_2$. Since $D$ is directed, there exists $\alpha_3 \succeq \alpha_1, \alpha_2$. For $\alpha \succeq \alpha_3$, we have $s_\alpha \in A \cap B$, so $A \cap B \in \mathcal{F}_s$. **Closure under supersets:** If $A \in \mathcal{F}_s$ and $A \subset B$, then there exists $\alpha_0$ with $s_\alpha \in A \subset B$ for all $\alpha \succeq \alpha_0$, so $B \in \mathcal{F}_s$. [/step]

[step:Show that the net converges to $x$ if and only if $\mathcal{F}_s$ converges to $x$] Recall that $\mathcal{F}_s$ converges to $x$ means: for every open set $U \in \tau$ with $x \in U$, we have $U \in \mathcal{F}_s$. Equivalently, the neighbourhood filter of $x$ is contained in $\mathcal{F}_s$. ($\Rightarrow$): If $s_\alpha \to x$, then for every open $U$ with $x \in U$, there exists $\alpha_0$ with $s_\alpha \in U$ for all $\alpha \succeq \alpha_0$. By definition, $U \in \mathcal{F}_s$. ($\Leftarrow$): If $\mathcal{F}_s$ converges to $x$, then every open neighbourhood $U$ of $x$ satisfies $U \in \mathcal{F}_s$, meaning there exists $\alpha_0$ with $s_\alpha \in U$ for all $\alpha \succeq \alpha_0$. This is the definition of $s_\alpha \to x$. The equivalence holds because "$s_\alpha$ is eventually in $A$" and "$A \in \mathcal{F}_s$" are the same statement by construction of $\mathcal{F}_s$. [/step]

[step:Show that $y$ is a cluster point of the net if and only if $y$ is a cluster point of $\mathcal{F}_s$]A point $y$ is a cluster point of $\mathcal{F}_s$ if every $F \in \mathcal{F}_s$ and every open neighbourhood $U$ of $y$ satisfy $F \cap U \neq \varnothing$. Equivalently, $y \in \overline{F}$ for every $F \in \mathcal{F}_s$. ($\Rightarrow$): Assume $y$ is a cluster point of the net: for every open $U$ containing $y$ and every $\alpha_0 \in D$, there exists $\alpha \succeq \alpha_0$ with $s_\alpha \in U$. Let $F \in \mathcal{F}_s$ and let $U$ be an open neighbourhood of $y$. There exists $\alpha_0 \in D$ with $s_\alpha \in F$ for all $\alpha \succeq \alpha_0$. By the cluster point property applied with this $\alpha_0$ and the neighbourhood $U$, there exists $\alpha \succeq \alpha_0$ with $s_\alpha \in U$. This $\alpha$ satisfies $s_\alpha \in F \cap U$, so $F \cap U \neq \varnothing$. ($\Leftarrow$): Assume $y$ is a cluster point of $\mathcal{F}_s$. Let $U$ be an open neighbourhood of $y$ and let $\alpha_0 \in D$. Define the tail set $T_{\alpha_0} := \{s_\alpha : \alpha \succeq \alpha_0\}$. Then $T_{\alpha_0} \in \mathcal{F}_s$ (by definition of eventuality filter). Since $y$ is a cluster point of $\mathcal{F}_s$, we have $T_{\alpha_0} \cap U \neq \varnothing$. So there exists $\alpha \succeq \alpha_0$ with $s_\alpha \in U$. This is the definition of $y$ being a cluster point of the net.[/step]

[guided]The cluster point equivalence is the "frequent" analogue of the convergence equivalence in the previous step, where "eventual" was used. The key observation is that the tail sets $T_{\alpha_0} = \{s_\alpha : \alpha \succeq \alpha_0\}$ belong to $\mathcal{F}_s$ by construction, and they generate $\mathcal{F}_s$ in the sense that every $F \in \mathcal{F}_s$ contains some tail set. The cluster point condition for $\mathcal{F}_s$ quantifies over all $F \in \mathcal{F}_s$, while the cluster point condition for the net quantifies over all $\alpha_0 \in D$ — but since the tail sets sit inside $\mathcal{F}_s$ and generate it (as a filter base), these conditions are equivalent. Formally, the backward direction uses only the tail sets $T_{\alpha_0} \in \mathcal{F}_s$, while the forward direction requires the full strength of $F \cap U \neq \varnothing$ for arbitrary $F \in \mathcal{F}_s$. The forward implication works because any such $F$ contains a tail set $T_{\alpha_0}$, and finding a net term in $T_{\alpha_0} \cap U$ automatically gives one in $F \cap U$.[/guided]

## Part 2: From filters to nets

[step:Verify that $D_\mathcal{F}$ is a directed set]Let $\mathcal{F}$ be a filter on $X$. Define \begin{align*} D_\mathcal{F} := \{(x, F) : F \in \mathcal{F},\, x \in F\}, \end{align*} ordered by $(x_1, F_1) \preceq (x_2, F_2)$ if and only if $F_2 \subset F_1$. We verify the directed set axioms. Reflexivity and transitivity of $\preceq$ follow from reflexivity and transitivity of $\subset$. For the directedness condition: given $(x_1, F_1)$ and $(x_2, F_2)$ in $D_\mathcal{F}$, the intersection $F_1 \cap F_2 \in \mathcal{F}$ (since $\mathcal{F}$ is closed under finite intersections). Since $F_1 \cap F_2 \in \mathcal{F}$, we have $F_1 \cap F_2 \neq \varnothing$ (since $\varnothing \notin \mathcal{F}$), so we may choose $x_3 \in F_1 \cap F_2$. Then $(x_3, F_1 \cap F_2) \in D_\mathcal{F}$, and $(x_3, F_1 \cap F_2) \succeq (x_1, F_1)$ and $(x_3, F_1 \cap F_2) \succeq (x_2, F_2)$ since $F_1 \cap F_2 \subset F_1$ and $F_1 \cap F_2 \subset F_2$.[/step]

[guided]The construction of $D_\mathcal{F}$ encodes a filter as a directed set by pairing each filter member $F$ with a "sample point" $x \in F$. The ordering by reverse inclusion on the second component ensures that moving forward in $D_\mathcal{F}$ means refining the filter — passing to smaller sets, just as convergence requires. Directedness depends on both the closure of $\mathcal{F}$ under finite intersections (to obtain $F_1 \cap F_2 \in \mathcal{F}$) and the properness of $\mathcal{F}$ (to guarantee $F_1 \cap F_2 \neq \varnothing$ and thus find a sample point). If we allowed the empty set in $\mathcal{F}$, we could not select $x_3$, and the construction would fail. Note that the ordering ignores the first component entirely: $(x_1, F_1) \preceq (x_2, F_2)$ depends only on $F_2 \subset F_1$. The first component is simply a "witness" that records which point of $F$ we are sampling. This is why the canonical net $s_{(x,F)} = x$ projects onto the first component — it reads off the witness.[/guided]

[step:Show that $\mathcal{F}$ converges to $x$ if and only if its canonical net converges to $x$] The canonical net is the map $s: D_\mathcal{F} \to X$ defined by $s_{(x,F)} := x$. ($\Rightarrow$): Assume $\mathcal{F}$ converges to $x$: every open neighbourhood $U$ of $x$ satisfies $U \in \mathcal{F}$. Let $V$ be an open neighbourhood of $x$. Then $V \in \mathcal{F}$, so $(x, V) \in D_\mathcal{F}$. For any $(y, G) \succeq (x, V)$, we have $G \subset V$, and $y \in G \subset V$, so $s_{(y,G)} = y \in V$. Thus the canonical net is eventually in $V$, and $s \to x$. ($\Leftarrow$): Assume $s_{(y,G)} \to x$. Let $U$ be an open neighbourhood of $x$. By convergence, there exists $(y_0, G_0) \in D_\mathcal{F}$ such that $s_{(y,G)} \in U$ for all $(y, G) \succeq (y_0, G_0)$. In particular, for every $F \in \mathcal{F}$ with $F \subset G_0$ and every $z \in F$, we have $(z, F) \succeq (y_0, G_0)$, so $z = s_{(z,F)} \in U$. Therefore $F \subset U$ for every $F \in \mathcal{F}$ with $F \subset G_0$. In particular, $G_0 \subset U$ (taking $F = G_0$, since every $z \in G_0$ satisfies $(z, G_0) \succeq (y_0, G_0)$ and thus $z \in U$). Since $G_0 \in \mathcal{F}$ and $G_0 \subset U$, the closure of $\mathcal{F}$ under supersets gives $U \in \mathcal{F}$. [/step]

[step:Show that $y$ is a cluster point of $\mathcal{F}$ if and only if $y$ is a cluster point of the canonical net]($\Rightarrow$): Assume $y$ is a cluster point of $\mathcal{F}$: for every $F \in \mathcal{F}$ and every open neighbourhood $U$ of $y$, we have $F \cap U \neq \varnothing$. Let $U$ be an open neighbourhood of $y$ and let $(x_0, F_0) \in D_\mathcal{F}$. We must find $(z, G) \succeq (x_0, F_0)$ with $s_{(z,G)} \in U$. Since $y$ is a cluster point, $F_0 \cap U \neq \varnothing$. Choose $z \in F_0 \cap U$. Then $(z, F_0) \in D_\mathcal{F}$ (since $z \in F_0 \in \mathcal{F}$), $(z, F_0) \succeq (x_0, F_0)$ (since $F_0 \subset F_0$), and $s_{(z, F_0)} = z \in U$. ($\Leftarrow$): Assume $y$ is a cluster point of the canonical net: for every open neighbourhood $U$ of $y$ and every $(x_0, F_0) \in D_\mathcal{F}$, there exists $(z, G) \succeq (x_0, F_0)$ with $s_{(z,G)} = z \in U$. Let $F \in \mathcal{F}$ and let $U$ be an open neighbourhood of $y$. Choose any $x_0 \in F$ (possible since $F \neq \varnothing$), so $(x_0, F) \in D_\mathcal{F}$. By the cluster point condition, there exists $(z, G) \succeq (x_0, F)$ with $z \in U$. Since $(z, G) \succeq (x_0, F)$, we have $G \subset F$, so $z \in G \subset F$. Combined with $z \in U$, this gives $z \in F \cap U$, so $F \cap U \neq \varnothing$.[/step]

[guided]The cluster point equivalences are the "frequent" counterparts of the convergence equivalences established in the previous step. For the forward direction: the cluster point condition for $\mathcal{F}$ says that every filter member $F$ meets every neighbourhood $U$ of $y$. To show the canonical net clusters at $y$, we need to find, past any given index $(x_0, F_0)$, a net term in $U$. We use $F_0$ itself as the filter member: since $F_0 \cap U \neq \varnothing$, pick $z \in F_0 \cap U$ and observe that $(z, F_0) \succeq (x_0, F_0)$ (because $F_0 \subset F_0$). This is valid because the ordering depends only on the filter-set component, not the point component. For the backward direction: given $F \in \mathcal{F}$ and a neighbourhood $U$ of $y$, we start from $(x_0, F) \in D_\mathcal{F}$ (choosing any $x_0 \in F$). The cluster point condition for the net produces $(z, G) \succeq (x_0, F)$ with $z \in U$. The inequality $(z, G) \succeq (x_0, F)$ means $G \subset F$, so $z \in G \subset F$. Combined with $z \in U$, we get $F \cap U \neq \varnothing$. Both directions exploit the same structural feature: the ordering on $D_\mathcal{F}$ remembers only the filter-set component, while the point component is a free witness that can be chosen to land in any desired set.[/guided]