The purpose of this section is to prove the following theorem.
Toward the proof of Theorem 3.1, we first prove a separation result for finite-dimensional Euclidean spaces.
Proof. For we denote by the dot product of x and y. The norm on R^{n} is given by . We imitate the argument of Lemma 3.1 of [5].
Put . Then C is a compact convex set in R^{n}. Since , we have . The function is continuous on C, so it follows in that there exists of minimum norm, i.e., for all .
We claim that
for all .
Suppose not.
Let
be such that
.
Consider
w=tz+(1-t)c where .
Since C is convex, we
have ,
hence
.
Expansion of
gives
Define by . Since , we may fix and such that c=b-a. Using our claim, it is easy to show that for all and . Thus A and B are strictly separated.
In order to reduce Theorem 3.1 to the finite-dimensional Euclidean case, we need some technical lemmas.
Proof. Reasoning in
,
put
and
Since V is open, there is a sequence of open balls
B((a_{m},b_{m}),r_{m}),
,
,
,
such that
We claim that
Since the condition (1) is , it follows by Lemma II.5.7 of [20] that is open. Therefore, the complementary set is closed. This proves our lemma.
Proof. Consider the compact space
where
Proof. Since K is compact, there is a sequence of points , , , such that for each . Let S be the bounded tree consisting of all finite sequences such that for all n< the length of . Construct a sequence of trees , , such that for each j there is a one-to-one correspondence between infinite paths g in T_{j} and points , the correspondence being given by . For details of the construction of the T_{j}'s, see Section IV.1 of [20].
Let be a primitive recursive pairing function which is onto and monotone in both arguments. Let be the interleaved tree, defined by putting if and only if for all j, where . Note that T is a bounded tree, the bounding function being given by h((j,n))=k_{n}+1. In order to show that T is infinite, we prove that for all m there exists of length m such that for all j and all length of , has at least one extension of length n in T_{j}. This statement is easily proved by induction on m, using the fact that each of the T_{j}'s is infinite.
Since T is an infinite bounded tree, it follows by Bounded König's Lemma in (see Section IV.1 of [20]) that T has an infinite path, f. Then for each j we have an infinite path f_{j} in T_{j} given by f_{j}(n)=f((j,n)). Thus we obtain a sequence of points where is a point of C_{j}.
Proof. We first prove that X' has a basis. By lemma 3.5, the
set of all linearly independent
is open.
By bounded
comprehension in
,
it follows that
It remains to prove that X' is a closed subspace of X. As a code for X' we may use Q^{n} identifying with . Thus X' is a subspace of X. The fact that X' is closed follows easily from Lemma 3.5.
We are now ready to prove Theorem 3.1.
Proof. [Proof of Theorem 3.1]
Reasoning within
,
let X, A, B be as in the hypotheses
of Theorem 3.1. We need to prove that A and B can be
separated. Since A is open, we may safely assume that
Since X is a separable Banach space, there exists a countable
vector space D over the rational field
Q such that
and D is dense in X. Since B is separably closed, there
exists a countable sequence
such that S is dense in
B. We may safely assume that
.
With this
assumption, consider the compact product space
Suppose we are given a finite set of conditions . Let be the elements of that are mentioned in . Let be the elements of S that are mentioned in . Let be the nonzero elements of D that are mentioned in . By Lemma 3.7, let X' be the finite-dimensional subspace of X spanned by . Let A' be the convex hull of . Let B' be the convex hull of . Note that and ; hence . Moreover A' and B' are compact. By Lemmas 3.7 and 3.3, there exists a bounded linear functional such that for all , and for all . In particular for all ; hence . Put for , and for . Then is a point of K which satisfies . This completes the proof.