Theorem: Kottman's Improvement of Riesz' Lemma

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be an infinite-dimensional normed vector space over $\GF$.
Then there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ such that $\norm {x_n}_X = 1$ for each $n \in \N$ and:
:$\norm {x_n - x_m}_X > 1$ for each $n \ne m$. 
That is, the Kottman constant $\map K X$ of $X$ satisfies $\map K X > 1$.

Proof:
We firstly take $\GF = \R$. 
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $x_1 \in X$ have $\norm {x_n}_X = 1$.
From Existence of Support Functional, there exists $f_1 \in X^\ast$ such that $\norm {f_1}_{X^\ast} = 1$ and:
:$\map {f_1} {x_1} = \norm {x_1}_X = 1$
We construct $\sequence {x_n}_{n \mathop \in \N}$ inductively, alongside a sequence $\sequence {f_n}_{n \mathop \in \N}$ in $X^\ast$. 
These will be such that:
:$\map {f_n} {x_n} = 1$ for each $n \in \N$
:$\map {f_j} {x_n} < 0$ for each $1 \le j < n$
:$\norm {f_n}_{X^\ast} = 1$ for each $n \in \N$.
Suppose that, for some $k \ge 1$, we have constructed $x_1, \ldots, x_k \in X$ and $f_1, \ldots, f_k \in X^\ast$ with:
:$\norm {x_j}_X = 1$ for each $1 \le j \le k$
and:
:$\map {f_j} {x_j} = 1$ for each $1 \le j \le k$
and that we have shown that $\set {f_1, \ldots, f_k}$ is linearly independent. 
We aim to construct $x_{k + 1} \in X$ and $f_{k + 1} \in X^\ast$ such that the construction may continue.
Since $\set {f_1, \ldots, f_k}$ is linearly independent, we have:
:$f_j \not \in \map \span {\set {f_i : i \ne j, \, i \le k} }$
From Condition for Linear Dependence of Linear Functionals in terms of Kernel, we have:
:$\ds \bigcap_{i \ne j, \, i \le k} \ker f_i \not \subseteq \ker f_j$
We can therefore take:
:$\ds y_j \in \bigcap_{i \ne j, \, i \le k} \ker f_i$
such that $\map {f_j} {y_j} \ne 0$. 
That is, $\map {f_j} {y_j} \ne 0$ yet $\map {f_j} {y_i} = 0$ for $i \ne j$. 
By replacing $y_j$ with $-y_j$ if necessary, we can take $\map {f_j} {y_j} < 0$. 
Take:
:$\ds y = \sum_{j \mathop = 1}^k y_j$
We then have:
:$\map {f_j} y = \map {f_j} {y_j} < 0$ for each $j \le k$.
From Intersection of Finitely Many Kernels of Linear Functionals in Infinite-Dimensional Vector Space is Infinite-Dimensional with Finite Codimension, we have that:
:$\ds \bigcap_{j \mathop = 1}^k \ker f_j \ne \set { {\mathbf 0}_X}$
Hence we can take:
:$\ds x \in \bigcap_{j \mathop = 1}^k \ker f_j \setminus \set { {\mathbf 0}_X}$
By the Reverse Triangle Inequality: Normed Vector Space, we have:
:$\norm {y + K x}_X \ge \cmod K \norm x_X - \norm y_X$
with $\norm x_X > 0$. 
Hence by taking: 
:$\ds K > \frac {2 \norm y_X} {\norm x_X}$
we have:
:$\norm {y + K x}_X > \norm y_X$
Now let $\lambda_1, \ldots, \lambda_n \in \R$ be such that $\lambda_j \ne 0$ for some $j$. 
Since $\set {f_1, \ldots, f_k}$ is linearly independent, we have:
:$\ds \sum_{j \mathop = 1}^k \lambda_j f_j \ne {\mathbf 0}_{X^\ast}$
We then have:
{{begin-eqn}}
{{eqn	| l = \cmod {\sum_{j \mathop = 1}^k \lambda_j \map {f_j} {y + K x} }
		| r = \cmod {\sum_{j \mathop = 1}^k \lambda_j \map {f_j} y}
		| c = $\map {f_j} x = 0$ for each $j$
}}
{{eqn	| o = \le
		| r = \norm {\sum_{j \mathop = 1}^k \lambda_j f_j}_{X^\ast} \norm y_X 
		| c = Fundamental Property of Norm on Bounded Linear Functional
}}
{{eqn	| o = <
		| r = \norm {\sum_{j \mathop = 1}^k \lambda_j f_j}_{X^\ast} \norm {y + K x}_X
}}
{{end-eqn}}
Since $\norm {y + K x}_X > \norm y_X > 0$, we can take:
:$\ds x_{k + 1} = \frac {y + K x} {\norm {y + K x}_X}$
with $\norm {x_{k + 1} }_X = 1$. 
By Existence of Support Functional, there exists $f_{k + 1} \in X^\ast$ such that:
:$\map {f_{k + 1} } {x_{k + 1} } = \norm {x_{k + 1} }_X = 1$
and $\norm {f_{k + 1} }_{X^\ast} = 1$. 
We show that $\set {f_1, \ldots, f_{k + 1} }$ is linearly independent.
{{WLOG}} suppose there exists $\lambda_1, \ldots, \lambda_n \in \R$ such that:
:$\ds f_{k + 1} = \sum_{j \mathop = 1}^k \lambda_j f_j$
We have that:
:$\ds \size {\sum_{j \mathop = 1}^k \lambda_j \map {f_j} {y + K x} } < \norm {\sum_{j \mathop = 1}^k \lambda_j f_j}_{X^\ast} \norm {y + K x}_X$
That is, by dividing through $\norm {y + K x}_X$:
:$\ds \size {\map {f_{k + 1} } {x_{k + 1} } } < 1$
This contradicts that $\map {f_{k + 1} } {x_{k + 1} } = 1$.
Hence $\set {f_1, \ldots, f_{k + 1} }$ is linearly independent.
It remains to show that $\map {f_j} {x_{k + 1} } < 0$ for each $1 \le j \le k$. 
We recall that by our choice $y$, we have:
:$\map {f_j} y < 0$ for each $1 \le j \le k$.
Since $\map {f_j} x = 0$ for each $1 \le j \le k$, we have that:
:$\map {f_j} {x_{k + 1} } < 0$ for each $1 \le j \le k$. 
Continuing this way, we can construct sequences $\sequence {x_n}_{n \mathop \in \N}$ and $\sequence {f_n}_{n \mathop \in \N}$ with $\norm {x_n}_X = 1$ and $\norm {f_n}_{X^\ast} = 1$ with:
:$\map {f_n} {x_n} = 1$ for each $n \in \N$
:$\map {f_j} {x_n} < 0$ for each $1 \le j < n$
:$\norm {f_n}_{X^\ast} = 1$ for each $n \in \N$.
Now take $m, n \in \N$ with $m \ne n$.
Suppose that $m > n$.
Then we have:
{{begin-eqn}}
{{eqn	| l = \norm {x_m - x_n}_X
		| o = \ge
		| r = \size {\map {f_n} {x_m - x_n} } 
		| c = Fundamental Property of Norm on Bounded Linear Functional
}}
{{eqn	| r = \size {\map {f_n} {x_m} - 1}
		| c = since $\map {f_n} {x_n} = 1$
}}
{{end-eqn}}
Since $\map {f_n} {x_m} < 0$ (since $n < m$), we have that:
:$\size {\map {f_n} {x_m} - 1} > 1$ 
Hence:
:$\norm {x_m - x_n}_X > 1$ for each $n, m \in \N$ with $n \ne m$.
In the case $\GF = \C$, we consider the realification $\struct {X_\R, \norm {\, \cdot \,}_X}$ of $X$.
From Realification of Infinite-Dimensional Complex Vector Space is Infinite-Dimensional, we have that $X_\R$ is infinite-dimensional.
Then  there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $X_\R$ such that $\norm {x_n}_X = 1$ for each $n \in \N$ and:
:$\norm {x_n - x_m}_X > 1$ for each $n \ne m$. 
The underlying vector space of both $X$ and $X_\R$ is the same, as is the norm, and hence we obtain the result for $X$.
{{qed}}
{{Namedfor|Clifford Alfons Kottman|name2 = Frigyes Riesz|cat = Kottman|cat2 = Riesz F}}