Homotopy Type Theory
limit of a net > history (Rev #16, changes)
Showing changes from revision #15 to #16:
Added | Removed | Changed
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
For Archimedean ordered fields
Let be an Archimedean ordered field and let
be the positive elements in . Given a directed type , an element is a limit of a net or that converges to if
The set of all limits of a net is defined as
A limit of a sequence is usually written as
For preconvergence spaces
Let be a preconvergence space. Given a directed type , an element is a limit of a net or that converges to if .
The set of all limits of a net is defined as
In homotopy type theory
For Archimedean ordered fields
Let be an Archimedean ordered field and let
be the positive elements in . Given a directed type , a term is a limit of a net or that converges to if comes with a term
The type of all limits of a net is defined as
A limit of a sequence is usually written as
For preconvergence spaces
Let be a preconvergence space. Given a directed type , a term is a limit of a net or that converges to if the proposition is contractible.
The type of all limits of a net is defined as
See also
Revision on April 18, 2022 at 17:47:47 by
Anonymous?.
See the history of this page for a list of all contributions to it.