Homotopy Type Theory
limit of a sequence > history (Rev #1, changes)
Showing changes from revision #0 to #1:
Added | Removed | Changed
Contents
Definition
For Archimedean ordered fields
Let be an Archimedean ordered field and let
be the positive elements in . A term is a limit of a sequence 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 sequential convergence spaces
Let be a sequential convergence space. A term is a limit of a sequence or that converges to if the proposition is contractible.
The type of all limits of a net is defined as
See also
Revision on June 10, 2022 at 01:35:58 by
Anonymous?.
See the history of this page for a list of all contributions to it.