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 premetric spaces
Let be a dense integral subdomain of the type rational numbers and let be and a - be the positive terms ofpremetric space . and be a -premetric space. 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:
Let and be -premetric spaces. 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 Most convergence general spaces 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: