[[!redirects sequentially 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 [[sequential convergence space]]. Then $S$ is a __sequentially Hausdorff space__ if for all [[sequence]]s $x \in S^\mathbb{N}$, the set of all [[limit of a net|limits]] of $x$ has at most one element $$isSequentiallyHausdorff(S) \coloneqq \forall x \in S^\mathbb{N}. \{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_{n \to \infty} (-)(n)$ as a [[partial function]] $$\lim_{n \to \infty} (-)(n) \in (\mathbb{N} \to S) \to_{\mathcal{U}} S$$ ### In homotopy type theory ### Let $S$ be a [[sequential convergence space]]. 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$$ ## Properties ## Every [[Archimedean ordered field]] is a sequentially Hausdorff space. ## See also ## * [[limit of a sequence]] * [[rational numbers]] * [[real numbers]]