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

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #6 to #7: Added | Removed | Changed

Contents

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

Definition

In Archimedean set ordered theory fields

Let F S F S be an a Archimedean preconvergence ordered space field. Then F S F S is a Hausdorff space if for all directed setsdirected typeI∈DirectedSet 𝒰I \in DirectedSet_\mathcal{U} s andI:𝒰I:\mathcal{U} and nets x : ∈IS I→F x:I x \to \in F S^I , the type set of alllimits of xx is has a at most one elementproposition

isHausdorff( F S)≔∏ I:𝒰∀isDirected(I∈DirectedSet 𝒰.∀x∈S I.{l∈S|isLimit S(x,l) × }∏ x:I→F≅ isProp ∅∨{l∈S|isLimit S(limx,l)}≅𝟙 isHausdorff(F) isHausdorff(S) \coloneqq \prod_{I:\mathcal{U}} \forall isDirected(I) I \times \in \prod_{x:I DirectedSet_\mathcal{U}. \to \forall F} x isProp(\lim \in x) S^I. \{l \in S \vert isLimit_S(x, l)\} \cong \emptyset \vee \{l \in S \vert isLimit_S(x, l)\} \cong \mathbb{1}

All where Archimedean ordered fields are Hausdorff spaces.𝟙\mathbb{1} is the singleton set.

Most general definition

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

Let SS be a type with a predicate →\to between the type of all nets in SS

lim∈NetsIn(S)→ 𝒰 +S\lim \in NetsIn(S) \to_{\mathcal{U}^+} S
∑ I:𝒰isDirected(I)×(I→S)\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)

In homotopy type theory

and LetSS itself. be Then aSSpreconvergence space . is Then aSS is a Hausdorff space if for all directed types I:𝒰I:\mathcal{U} and nets x:I→Sx:I \to S, the type of all limits of xx is has a at most one elementproposition

isHausdorff(S)≔∏ I:𝒰isDirected(I)×∏ x:I→SisProp(∑ 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} x isLimit_S(x, \to l)\right) l\right)

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

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

Properties

All Archimedean ordered fields are Hausdorff spaces.

See also

Revision on April 14, 2022 at 05:31:16 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (3 more)Previous revision (6 more)Current version of pageHide changesHistory (9 revisions)Rollback Source