This is a follow-up on my previous question: Generalizing the idea of sequences
Suppose $S$ is a non-empty set with no metric defined on it. Which of the following definitions could be extended so as to still have meaning on the set $S$ with no metric? Which of the definitions could not?
Sequence on $S$
Constant sequence on $S$
Eventually constant sequence on $S$
Convergent sequence on $S$
Cauchy sequence on $S$
Subsequence of a sequence on $S$
Suppose $S$ is a topological space. Define $f: D \to S$, where
$D$ is a set that satisfies the following properties:
$\forall x \in D, x \le x$.
$\forall x,y,z \in D: (x \le y) \land (y \le z) \Rightarrow x \le z$.
$\forall x,y \in D, \exists z \in D : (x \le z) \land (y \le z)$.
This means that $D$ is a directed set.
Let $D=\mathbb{N}$ with its usual ordering relation $\le$, then $f$ is a net in $S$ indexed by $(\mathbb{N},\le)$, which means that $f$ is a sequence in $S$.
Note that $f$ is a net in $S$ whose domain $D$ consists of elements that denote its indices.
Also, the values of the net are denoted by $f_{\lambda}:=f(\lambda)$ and the net is denoted by $(f_{\lambda})_{\lambda \in D}$.
Definition : Convergent sequence on $S$
We say that a net $(f_{\lambda})_{\lambda \in D}$ in $S$ converges to a point $c \in S$ provided that for every neighborhood $N$ of $c$, $\exists \lambda_0 \in D$ such that $\forall \lambda \ge \lambda_0: f(\lambda) \in N$. This means that the net is eventually in $N$.
Definition: Subsequence of a sequence on S
A subnet (i.e. subsequence of a sequence on S) of $(f_{\lambda})_{\lambda \in D}$ is a net $(f_{\lambda_\alpha})_{\alpha \in M}$ for some directed set $M$, where $\lambda_{\alpha}:=\varphi(\alpha)$, and the function $\varphi: M \to D$ is non-decreasing and cofinal.
Note that cofinal means that $\forall \lambda \in D: \exists \alpha \in M : \varphi(\alpha) \ge \lambda$.
And that $\varphi$ non-decreasing means that $\forall \alpha_1, \alpha_2 \in M: (\alpha_1 \le_M \alpha_2) \Rightarrow (\varphi(\alpha_1) \le_D \varphi(\alpha_2))$.
Definition: Cauchy Sequence
We say that $(f_{\lambda})_{\lambda \in D}$ is a Cauchy net (i.e. Cauchy sequence) if for every uniform space $V, \exists \lambda \in D: \forall \varepsilon, \sigma \ge \lambda$, we have $(f_{\varepsilon},f_{\sigma}) \in V$.
Definition: Constant sequence on S
A sequence $(f_{\lambda})_{\lambda \in D}$ is called a constant sequence in $S$ provided $\forall \lambda \in D, f_\lambda=f_0$.
Definition: Eventually constant sequence on S
A sequence $(f_{\lambda})_{\lambda \in D}$ is called eventually constant if $\exists \lambda \in D, \forall \alpha \in D, [\alpha \ge \lambda \Rightarrow f_\alpha=f_\lambda]$.
Is this correct?
Most of this I can agree with and is pretty standard in topology.
For the constant net and eventually constant net I’d put them more like:
$$\exists s_0 \in S: \forall \lambda \in D: f(\lambda)=s_0$$ and
$$\exists s_0 \in S:\exists \lambda_0 \in D: \forall \lambda \ge \lambda_0: f(\lambda)=s_0$$ where we can use $f_\lambda$ for $f(\lambda)$ if you prefer.
For constant net/sequence you assume that $D$ has some element named $0$ (you write $f_0$) which is unwarranted in general. So I prefer to focus on the constant value $s_0$ instead. Nitpicking really.
For Cauchy nets we need to quantify $V$ over the set of entourages of some fixed uniformity $\mathcal{U}$ on $S$, but then it’s OK. You say “for every uniform space $V$” which makes no sense at all, but just like when you fix a topology on $S$ to talk about its neighbourhoods (so we can talk about convergence which on a bare set we cannot) we also fix a uniformity on $S$ when talk about Cauchy nets in it. Of course if $S$ has a metric it has both of them in a standard way. You could also do uniformities in an equivalent way using uniform covers and then the definition of Cauchy net needs a small modification as well. But in the entourage based definition we say that $f$ is. Cauchy iff:
$$\forall V \in \mathcal{U}: \exists \lambda_0 \in D: \forall \lambda,\mu \in D: (\lambda \ge \lambda_0 \land \mu \ge \lambda_0) \to (f_\lambda, f_\mu) \in V$$
For subnets you’re using the “Willard definition” while I was “raised” using the Kelley definition (the first to define nets in topology, so it’s the tradition): the “connecting map” $\varphi: M \to D$ then need not be increasing but needs to obey the following condition:
$$\forall \lambda \in D: \exists \mu_0 \in M: \forall \mu \in M: (\mu \ge_M \mu_0) \to (\varphi(\mu) \ge_D \lambda)$$ which says that the image of $\varphi$ is sort of consistently cofinal in $D$: you go further along in $D$ by going beyond some point in $M$. Your definition (which is quite commonly used as it’s easier to formulate, maybe more intuitive, and was used in a popular textbook as Willard’s) allows one to prove the same results (Every subnet of a convergent net has the same limit, if a net has an accumulation point it has a convergent subnet converging to it, $S$ is compact iff every net has a convergent subnet etc) as with the Kelley one. For subsequences (so restricting the domains to $\Bbb N$ in the usual order) these definitions give the same generalisation as subsequence does.
You could also look at the more modern and convenient definition of AA-subnets, these are compared in this nice PDF notes. Subnets of a given net do not form a set (but a so-called class) which can be inconvenient. I like nets for some arguments but filters for others (another way to define convergence), but it’s a matter of convenience/taste, just so you know that your version of the definition is not the only one that’s possible.
So most of your definitions were essentially correct (modulo nitpicks) and the subnet one is one of the popular options..