Homotopy Type Theory Hausdorff space > history (changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

Contents

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

$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 fields are Hausdorff spaces.