be the positive elements in . The limit of a function approaching an element is an element such that for all directed sets and nets where is the limit of , is the limit of , or written in type theory:
where the predicates
The limit is usually written as
In preconvergence spaces
Let and be preconvergence spaces. The limit of a function approaching an element is an element such that for all directed sets and nets where is a limit of , is a limit of , or written in type theory:
be the positive elements in . 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 preconvergence spaces
Let and be preconvergence spaces. 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: