A net clusters at $x$ iff the "filter generated by the net" clusters at $x$

Question

Let $\langle x_\lambda \rangle_{\lambda\in\Lambda}$ be a net. Let $\mathscr{F}_{x_\lambda}$ be the filter generated by the net $\langle x_\lambda \rangle$, i.e. the generated by the filter base $\mathscr{C}_{x_\lambda} = \{\{x_{\lambda }:\lambda\geq\mu\}\}_{\mu\in\Lambda}$.

What I would like to show is,

$\langle x_\lambda \rangle_{\lambda\in\Lambda}$ clusters at $x$ iff $\mathscr{F}_{x_\lambda}$ clusters at $x$.

Proof:

($\Rightarrow$)Note,

$$\left(\forall U\in\mathscr{U}_x,\exists C\in\mathscr{C}_{x_\lambda}: C\subseteq U\right)\iff\left(\mathscr{C}_{x_\lambda}\to x\right)\iff\left(\mathscr{F}_{x_\lambda}\to x\right) \implies \left(\mathscr{F}_{x_\lambda}\text{ clusters at } x\right).$$

Therefore, it is enough to show that $\forall U\in\mathscr{U}_x,\exists C\in\mathscr{C}_{x_\lambda}: C\subseteq U$.

So, let $U\in\mathscr{U}_{x}$. By definition of $\langle x_\lambda \rangle_{\lambda\in\Lambda}$ clustering at $x$ and $U$ and open nbhd of $x$,

$$\forall\mu\in\Lambda, \exists \lambda\in\Lambda: \lambda\geq\mu \text{ and } x_{\lambda}\in U.$$

This implies that $C:=\{x_{\lambda}:\lambda\geq\mu\}\subseteq U$. As $U$ was arbitrary and $C\in\mathscr{C}_{x_\lambda}: C\subseteq U$, this direction is done.

($\Leftarrow$) Suppose $\mathscr{F}_{x_{\lambda}}$ clusters at $x$. Then for $U\in\mathscr{U}_x$ and $F\in\mathscr{F}_{x_{\lambda}}$, we have $U\cap F\neq\emptyset$. By def. of $F\in\mathscr{F}_{x_{\lambda}}$, there exists $C\in\mathscr{C}_{x_{\lambda}}: C\subseteq F$ hence $U\cap C\neq\emptyset$. By def. of $\mathscr{C}_{x_{\lambda}}$, this means that there exists $\{x_{\lambda}:\lambda\geq\mu\}$

$$U\cap\{x_{\lambda}:\lambda\geq\mu\}\neq\emptyset.$$

However, my question is, how does this imply "for each $\mu$, there is a $\lambda$ such that $\lambda\geq\mu$ and $x_{\lambda}\in U$"? More specifically, is appears to me that this implies an existence of $\mu$ rather than for each $\mu$.

Answer 1

Slowly unwrap the (correct!) definitions:

Suppose $(x_\lambda)_{\lambda \in \Lambda}$ cluster at $x$. Then $\mathcal{F}$ (I leave off the subscript) clusters at $x$ too, which means that every neighbourhood of $x$ intersects every set from the filterbase.

So let $O$ be an open neighbourhood of $x$, and let $C_\mu:=\{x_\lambda: \lambda \ge \mu\}$ be a set from the filterbase for some $\mu \in \Lambda$.

Now apply the net-cluster definiton at $x$ to $U$ and $\mu$, to get $\mu' \ge \mu$ such that $x_{\mu'} \in U$ and then $x_{\mu'} \in U \cap C_\mu$ as required. So we're done.

The reverse is very similar.