Contents

Definition

In Archimedean ordered fields

Let $F$ be an Archimedean ordered field. Then $F$ is a sequentially Hausdorff space if for all sequences $x:\mathbb{N} \to F$, the type of all limits of $x$ is a proposition

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 sequences $x:\mathbb{N} \to S$, the type of all limits of $x$ is a proposition

One could directly define the limit $\lim_{n \to \infty} (-)(n)$ as a partial function

See also

• limit of a net
• rational numbers
• real numbers
• Hausdorff space