[[!redirects sequentially Hausdorff]] #Contents# * table of contents {:toc} ## Definition ## ### In Archimedean ordered fields ### Let $F$ be an [[Archimedean ordered field]]. Then $F$ is a __sequentially Hausdorff space__ if for all [[sequence]]s $x:\mathbb{N} \to F$, the type of all [[limit of a net|limits]] of $x$ is a [[proposition]] $$isSequentiallyHausdorff(F) \coloneqq \prod_{x:\mathbb{N} \to F} isProp(\lim_{n \to \infty} x(n))$$ All Archimedean ordered fields are sequentially Hausdorff spaces. ### Most general definition ### Let $S$ be a type with a [[predicate]] $\to$ between the type of sequences in $S$, $\mathbb{N} \to S$, and $S$ itself. Then $S$ is a __sequentially Hausdorff space__ if for all [[sequence]]s $x:\mathbb{N} \to S$, the type of all [[limit of a net|limits]] of $x$ is a [[proposition]] $$isSequentiallyHausdorff(S) \coloneqq \prod_{x:\mathbb{N} \to S} isProp\left(\sum_{l:S} x \to l\right)$$ One could directly define the limit $\lim_{n \to \infty} (-)(n)$ as a [[partial function]] $$\lim_{n \to \infty} (-)(n): (\mathbb{N} \to S) \to_{\mathcal{U}} S$$ ## See also ## * [[limit of a net]] * [[rational numbers]] * [[real numbers]] * [[Hausdorff space]]