Homotopy Type Theory Hausdorff space > history (changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

Let SS be a preconvergence space. Then SS is a Hausdorff space if for all directed sets IDirectedSet 𝒰I \in DirectedSet_\mathcal{U} and nets xS Ix \in S^I, the set of all limits of xx has at most one element

isHausdorff(S)IDirectedSet 𝒰.xS I.{lS|isLimit S(x,l)}{lS|isLimit S(x,l)}𝟙isHausdorff(S) \coloneqq \forall I \in DirectedSet_\mathcal{U}. \forall x \in S^I. \{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\lim as a partial function

limNetsIn(S) 𝒰 +S\lim \in NetsIn(S) \to_{\mathcal{U}^+} S

In homotopy type theory

Let SS be a preconvergence space. Then SS is a Hausdorff space if for all directed types I:𝒰I:\mathcal{U} and nets x:ISx:I \to S, the type of all limits of xx has at most one element

isHausdorff(S) I:𝒰isDirected(I)× x:ISisProp( l:SisLimit S(x,l))isHausdorff(S) \coloneqq \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isProp\left(\sum_{l:S} isLimit_S(x, l)\right)

One could directly define the limit lim\lim as a partial function

lim:( I:𝒰isDirected(I)×(IS)) 𝒰 +S\lim: \left(\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)\right) \to_{\mathcal{U}^+} S

or as a family of partial functions:

p:isDirected(I)lim i:I,i()(i):(IS) 𝒰Sp:isDirected(I) \vdash \lim_{i:I, i \to \infty} (-)(i): (I \to S) \to_\mathcal{U} S

Properties

All Archimedean ordered fields are Hausdorff spaces.

See also

Last revised on June 10, 2022 at 01:41:50. See the history of this page for a list of all contributions to it.