Homotopy Type Theory Hausdorff space > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In ~~premetric~~ Archimedean ~~spaces~~ ordered fields
- Most general definition
See also

Definition

In premetric Archimedean spaces ordered fields

Let $R F$ R F be a an ~~dense~~ ~~integral~~ ~~subdomain~~ of ~~the~~ ~~rational~~ Archimedean ~~numbers~~ ordered field . Then $ℚ F$ ~~\mathbb{Q}~~ F ~~and~~ is a ~~$R_{+}$~~ Hausdorff space be if ~~the~~ for ~~positive~~ all ~~terms~~ of ~~$R$~~ directed type . s $I:\mathcal{U}$ and nets $x:I \to F$ , the type of all limits of $x$ is a proposition

~~Let $S$ be an $R_{+}$ -premetric 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$ is a proposition~~

isHausdorff(F) \coloneqq \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to F} isProp(\lim x)

~~$isHausdorff(S) \coloneqq \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isProp(\lim x)$~~

All Archimedean ordered fields are Hausdorff spaces.

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 types $I:\mathcal{U}$ and nets $x:I \to S$ , the type of all 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

Homotopy Type Theory Hausdorff space > history (Rev #5, changes)

Contents

Definition

In premetric Archimedean spaces ordered fields

Most general definition

See also