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

Showing changes from revision #3 to #4: 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 sequential convergence space. Then SS is a sequentially Hausdorff space if for all sequences xS x \in S^\mathbb{N}, the set of all limits of xx has at most one element

isSequentiallyHausdorff(S)xS .{lS|isLimit S(x,l)}{lS|isLimit S(x,l)}𝟙isSequentiallyHausdorff(S) \coloneqq \forall x \in S^\mathbb{N}. \{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 n()(n)\lim_{n \to \infty} (-)(n) as a partial function

lim n()(n)(S) 𝒰S\lim_{n \to \infty} (-)(n) \in (\mathbb{N} \to S) \to_{\mathcal{U}} S

In homotopy type theory

Let SS be a sequential convergence space. Then SS is a sequentially Hausdorff space if for all sequences x:Sx:\mathbb{N} \to S, the type of all limits of xx is a proposition

isSequentiallyHausdorff(S) x:SisProp( l:Sxl)isSequentiallyHausdorff(S) \coloneqq \prod_{x:\mathbb{N} \to S} isProp\left(\sum_{l:S} x \to l\right)

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

lim n()(n):(S) 𝒰S\lim_{n \to \infty} (-)(n): (\mathbb{N} \to S) \to_{\mathcal{U}} S

Properties

Every Archimedean ordered field is a sequentially Hausdorff space.

See also

Revision on June 15, 2022 at 21:10:40 by Anonymous?. See the history of this page for a list of all contributions to it.