# Show constructively that the sequence definition of continuity implies the epsilon-delta definition

As I understand it, continuity of a real valued function f at a point x can equivalently be defined in terms of sequences or in the epsilon-delta way.

Sequence Definition: For every Cauchy sequence $\{x_i\}$ converging to x, $\{f(x_i)\}$ is a Cauchy sequence converging to $f(x)$.

Epsilon-Delta Definition: $\forall\epsilon>0,\exists\delta>0$ st $|x-x_0|<\delta\implies|f(x)-f(x_0)|<\epsilon$

I want to show constructively that the sequence definition implies the epsilon-delta definition. I see how to do this by showing the contrapositive (or essentially in the same way by using proof by contradiction) but I don't see how to do this proof constructively. I'll mention that I'm not 100% clear on the exact meaning of 'constructive', but I am using it to mean neither by contrapositive nor by contradiction.

One preliminary ideas: Fix $\epsilon$. Index the set of all sequences converging to x by j and let J be the corresponding index set. So $x_{ij}$ is the i'th element of sequence indexed by j converging to x. For each j, there is a $\delta_j>0$ such that $|x_{ij} -x|<\delta_j\implies|f(x_{ij})-f(x)|<\epsilon$ because of the following. By the hypothesis, each sequence j has a spot $m_j$ past which (inclusive) all elements in the sequence map to something within $\epsilon$ of $f(x)$. The element in this spot is $x_{m_jj}$. Then $|x_{ij}-x|<min[|x_{1j}-x|,|x_{2j}-x|,...,|x_{m_{j-1}}|]\implies i\geq m_j\implies|f(x_{ij})-f(x)|<\epsilon$. Therefore, $\delta_j=min(|x_{1j}-x|,|x_{2j}-x|,...,|x_{m_{j-1}}|)$ Define $A=\{\delta_j\}_{j\epsilon J}$. If we can show $supA$ exists, it will be our $\delta$ since each point in the domain of f is in some sequence converging to $x$.

I'm not sure how to use the hypothesis more usefully.

Please help. Thanks very much. Alex

• To prove it requires a weak form of the Axiom of Choice. The result cannot be proved in ZF. So for many notions of constructive, there is no constructive proof. Jun 5, 2015 at 4:55
• @AndréNicolas Gottit. Thanks. Jun 5, 2015 at 5:30
• You are welcome. I am sure this has been discussed on MSE. A (Google, maybe MSE) search should do it, sequential continuity axiom of choice. Jun 5, 2015 at 5:36