[[!redirects Hausdorff]] #Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|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 [[net]]s $x \in S^I$, the set of all [[limit of a net|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 type]]s $I:\mathcal{U}$ and [[net]]s $x:I \to S$, the type of all [[limit of a net|limits]] of $x$ has at most one element $$isHausdorff(S) \coloneqq \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isProp\left(\sum_{l:S} isLimit_S(x, l)\right)$$ One could directly define the limit $\lim$ as a [[partial function]] $$\lim: \left(\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)\right) \to_{\mathcal{U}^+} S$$ or as a family of partial functions: $$p:isDirected(I) \vdash \lim_{i:I, i \to \infty} (-)(i): (I \to S) \to_\mathcal{U} S$$ ## Properties ## All [[Archimedean ordered field]]s are Hausdorff spaces. ## See also ## * [[preconvergence space]] * [[limit of a net]] * [[rational numbers]] * [[real numbers]] * [[sequentially Hausdorff space]] * [[Hausdorff ring]]