Showing changes from revision #13 to #14:
Added | Removed | Changed
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In rational set numbers theory
Let be the rational numbers and let be the type of positive rational numbers. Given a directed type , a term is a limit of a net or that converges to if comes with a term
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
In Archimedean ordered fields
For preconvergence spaces
Let be an a Archimedean preconvergence ordered space field . and Given let a be the type of positive rational numbers. Given a directed type , a term is a limit of a net or that converges to if the proposition comes is with a termcontractible.
The type of all limits of a net is defined as
A limit of a sequence is usually written as
Most general definition
Let be a type with a predicate between the type of all nets in
and itself.
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