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

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In premetric spaces
- In Most ~~convergence~~ general ~~spaces~~ definition
See also

Definition

In premetric spaces

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and $R_{+}$ be the positive terms of $R$ .

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

p:\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isProp(\lim x)

In Most convergence general spaces 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

p:\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isProp(\lim x)

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

Contents

Definition

In premetric spaces

In Most convergence general spaces definition

See also