todo:
Rather define the set of all sequences which have a limit in the below sense
this is the domain of “lim” though of as function (on all sequences it would be a partial function)
| context | $\langle X,d_X\rangle$ … metric space |
| context | $\langle Y,d_Y\rangle$ … metric space |
| context | $f:X\to Y$ |
| context | $\xi\in X$ |
| definiendum | $\mathrm{lim}_{x\to \xi}\ f(x)\equiv y_\xi$ |
| range | $\varepsilon,\delta\in \mathbb R_+^*$ |
| postulate | $\forall\varepsilon.\ \exists \delta.\ \forall x.\ [\ 0<d_X(x,\xi)<\delta\ ] \Rightarrow [\ d_Y(f(x),y_\xi)<\varepsilon\ ]$ |