

Heine continuity implies Cauchy continuity without the Axiom of Choice
On this page we state and prove that every Heine continuous real function is also Cauchy continuous. In our proof we do not use the Axiom of Choice.
Two Definitions of ContinuityIn the context when f:R>R is a real function and x is a point on the real line, there are two most widely used definitions of continuity: Cauchy continuity (epsilondelta continuity) and Heine continuity (sequential continuity):
/\(e>0) \/(d>0) /\(y:R) [ xy<d => f(x)f(y)<e ].
/\(a:N>R) [ lim(n>oo) a(n) = x => lim(n>oo) f(a(n)) = f(x) ].
Introduction
Let f:R>R be a real function. Let x be a point on the real line. The Axiom of Choice is not needed to prove that if f is Cauchy continuous at x then f is Heine continuous at x. In fact, this is an easy straightforward proof.
Now, in order to prove the converse (if f is Heine continuous at x then f is Cauchy continuous at x) one needs to employ the Axiom of Choice. Again the proof is very easy: suppose that f is not Cauchy continuous and by the Axiom of Choice obtain a sequence whose existence contradicts Heine continuity.
However, if we suppose that f is Heine continuous on some neighborhood of x (= Heine continuous at each point of this neighborhood) then we can derive Cauchy continuity at x without employing the Axiom of Choice.
Statement of the Theorem and Proof
Fact 1. There exists (by construction  without the Axiom of Choice) a choice function for the set of all rational numbers (denoted Q). Formally:
\/(F) [ F:P(Q)\{O}>Q and /\(A:P(Q)\{O}) (F(A):A) ].
Proof. Identify rational numbers with ordered pairs of integers so that (m,n) corresponds to the rational number m/n. Imagine those pairs as a set of points on the plane and write a simple computer program which spirals outward from the origin visiting each point. Now, to every nonempty subset of Q we assign the number that will be first reached by our spiraling algorithm and thus we have a choice function for Q.
Fact 2. For every real number x there exists (by construction  without the Axiom of Choice) a sequence of rational numbers which converges to x. Formally:
/\(x:R) \/(a:N>Q) [ lim(n>oo) a(n) = x ].
Proof. Take the sequence of truncated decimal expansions of x so that the nth element of this sequence contains the first n digits of the decimal expansion of x and then zeros ad infinitum. This is then a sequence of rational numbers which converges to x.
Theorem 3. If f:Q>R is Heine continuous at x:Q then f is Cauchy continuous at x (without using the Axiom of Choice).
Proof. Conduct this proof yourself along the lines sketched in the introduction. This time you will not need the Axiom of Choice to obtain the sequence whose existence contradicts Heine continuity because you will be able to define this sequence by applying Fact 1.
Theorem 4. If f:(a,b)>R is Heine continuous at each point in the open interval (a,b) and x lies in (a,b) then f is Cauchy continuous at x.
Proof.
We want to show that /\(e>0) \/(d>0) /\(y:(a,b)) [ xy<d => f(x)f(y)<e ]. Let us argue by contradiction. Suppose that there exists an e>0 such that (4.1) /\(d>0) \/(y:(a,b)) [ xy<d and f(x)f(y)>=e ]. By Theorem 3, the restriction of f to the rational numbers in (a,b) is Cauchy continuous. So there exists a d>0 such that (4.2) /\(y:(a,b)nQ) [ xy<d => f(x)f(y)<e/2 ]. By 4.1, there exists a y:(a,b) such that xy<d and f(x)f(y)>=e. By Fact 2, there exists a sequence y[n] contained in (a,b)nQ such that lim(n>oo) y[n] = y. By 4.2, we have that (4.3) /\(n:N) [ f(x)f(y[n])<e/2 ]. Since f is Heine continuous at y, we have that lim(n>oo) f(y[n]) = f(y). Hence by 4.3, f(x)f(y)<=e/2. But we earlier had that f(x)f(y)>=e. This contradiction completes the proof.
See also