Homotopy Type Theory
sequentially Hausdorff space > history (Rev #3, changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
Let be a preconvergence sequential convergence space. Then is a sequentially Hausdorff space if for all sequences , the set of all limits of has at most one element
where is the singleton set.
One could directly define the limit as a partial function
In homotopy type theory
Let be a preconvergence sequential convergence space. Then is a sequentially Hausdorff space if for all sequences , the type of all limits of is a proposition
One could directly define the limit as a partial function
Properties
Every Hausdorff space and thus every Archimedean ordered field is a sequentially Hausdorff space.
See also
Revision on June 10, 2022 at 01:50:02 by
Anonymous?.
See the history of this page for a list of all contributions to it.