Net in a Type

A net in a type $X$ is a function $f:D\to X$ from a Directed Set $D$. Nets generalize the notion of a sequence $x_{n}:\mathbb{N}\to X$, and are used to formalize the notion of a convergence in topology.

Nets have a couple of benefits when compared to sequences:

• A sequence can only approach a point from a single direction, whereas a net can approach a point from many directions at once.
• A sequence can only reach countably deep into a space, whereas nets can go uncountably deep.

In other words, sequences fail to detect the topology of general topological spaces: for instance, Sequentially Compactness is unrelated to Compactness.