[[!redirects Hausdorff]] #Contents# * table of contents {:toc} ## Definition ## ### In premetric spaces ### Let $R$ be a dense integral subdomain of the [[rational numbers]] $\mathbb{Q}$ and $R_{+}$ be the positive terms of $R$. Let $S$ be an $R_{+}$-[[premetric 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$ is a [[proposition]] $$isHausdorff(S) \coloneqq \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isProp(\lim x)$$ ### Most general definition ### Let $S$ be a type with a [[predicate]] $\to$ between the type of all nets in $S$ $$\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)$$ and $S$ itself. 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$ is a [[proposition]] $$isHausdorff(S) \coloneqq \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isProp\left(\sum_{l:S} x \to 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$$ ## See also ## * [[limit of a net]] * [[rational numbers]] * [[real numbers]]