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 be a preconvergence space. Then is a Hausdorff space if for all directed sets and nets , 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 space. Then is a Hausdorff space if for all directed types and nets , the type of all limits of has at most one element
One could directly define the limit as a partial function
or as a family of partial functions:
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.