Cauchy criterion for a function limit (source code)

= Cauchy criterion for a function limit
{title2=$\lim_{h\to0^+}F(h)\text{ exists}\iff\forall\varepsilon>0\ \exists\delta>0:\ d(F(h),F(k))<\varepsilon\ (0<h,k<\delta)$}

For a <function> $F:(0,1)\to Z$ into a <complete metric space>, the displayed pairwise condition is equivalent to existence of a limit as $h\to0^+$. Necessity follows from the <triangle inequality>. For sufficiency, the values $F(1/(n+1))$ form a <Cauchy sequence>, hence converge to some $z\in Z$. Given $\varepsilon>0$, use the pairwise condition with $\varepsilon/2$ and then send $n\to\infty$ in $d(F(h),F(1/(n+1)))<\varepsilon/2$. This gives $d(F(h),z)\leq\varepsilon/2<\varepsilon$ for every sufficiently small positive $h$.