Let be the rational numbers and let be the positive rational numbers. The limit of a function approaching a term is a term such that for all directed types and nets where is the limit of , is the limit of , or written in type theory:
where
The limit is usually written as
In Archimedean ordered fields
Let be an Archimedean ordered field and let be the positive terms of . The limit of a function approaching a term is a term such that for all directed types and nets where is the limit of , is the limit of , or written in type theory:
where
The limit is usually written as
Most general definition
Let be a type with a predicate between the type of all nets in
and itself, and let be a type with a predicate between the type of all nets in
and itself.
The limit of a function approaching a term is a term such that for all directed types and nets where is a limit of , is a limit of , or written in type theory: