Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In Archimedean ordered fields

Let $F$ be an Archimedean ordered field. The limit of a function $f:\F \to F$ approaching a term $c:F$ is a term $L:F$ such that for all directed types $I$ and nets $x:I \to F$ where $c$ is the limit of $x$, $L$ is the limit of $f \circ x$, or written in type theory:

where

The limit is usually written as

In preconvergence spaces

Let $S$ and $T$ be preconvergence spaces. The limit of a function $f:S \to T$ approaching a term $c:S$ is a term $L:T$ such that for all directed types $I$ and nets $x:I \to S$ where $c$ is a limit of $x$, $L$ is a limit of $f \circ x$, or written in type theory:

In function limit spaces

Let $T$ be a function limit space and let $S \subseteq T$ be a subtype of $T$. The limit of a function $f:S \to T$ approaching $c:S$ is a term $L:T$ such that the limit of $f$ approaching $c:S$ is equal to $L$:

We define the type of functions with limits approaching $c$ as the dependent type

See also

• net
• Archimedean ordered field
• limit of a net
• pointwise continuous function