Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

Let $S$ be a preconvergence space. Then $S$ is a Hausdorff space if for all directed sets $I \in DirectedSet_\mathcal{U}$ and nets $x \in S^I$, the set of all limits of $x$ has at most one element

$isHausdorff(S) \coloneqq \forall I \in DirectedSet_\mathcal{U}. \forall x \in S^I. \{l \in S \vert isLimit_S(x, l)\} \cong \emptyset \vee \{l \in S \vert isLimit_S(x, l)\} \cong \mathbb{1}$

where $\mathbb{1}$ is the singleton set.

One could directly define the limit $\lim$ as a partial function

$\lim \in NetsIn(S) \to_{\mathcal{U}^+} S$

In homotopy type theory

Let $S$ be a preconvergence space. Then $S$ is a Hausdorff space if for all directed types $I:\mathcal{U}$ and nets $x:I \to S$, the type of all limits of $x$ has at most one element