If a metric space has the limit point property, is it separable? (ZF + AC$_\omega$)
I'm struggling with this problem for a week.
I'm talking about this in Metric space.
Here's the part of argument in Rudin PMA p.45; Let $X$ be limit point compact. Fix $\epsilon>0$ and $x_0 \in X$. Having chosen $x_0,\ldots,x_j \in X$, choose $x_{j+1}$, if possible, so that $d(x_i,x_{j+1})≧\epsilon$ for $i=0,\ldots,j$. Then this process must stop after a finite number of steps.
Here, Dependent Choice is used.
I know that ‘Limit point property $\Rightarrow$ separable’ is unprovable in ZF. (You can see this: If every infinite subset has a limit point in a metric space $X$, then $X$ is separable (in ZF))
I want to prove this in ZF+AC$_\omega$. Help.
So far, I proved that [Limit point compact $\Rightarrow$ separable] $\Rightarrow$ [Limit point compact $\Rightarrow$ Compact].
I need this to complete my proof.
Countable choice is sufficient. Separability is an easy consequence of total boundedness. Suppose that $X$ is not totally bounded. Then there is an $r>0$ such that for each $n\in\Bbb Z^+$,
$$X_n=\left\{\langle x_1,\dots,x_n\rangle\in X^n:d(x_i,x_j)\ge r\text{ for }1\le i<j\le n\right\}\ne\varnothing\;.$$
By countable choice there is some $\langle a_n:n\in\Bbb Z^+\rangle\in\prod_nX_n$. For $n\in\Bbb Z^+$ let $a_n=\langle x^n_i,\dots,x^n_n\rangle$. Now concatenate the $a_n$ to form an infinite sequence
$$\sigma=\langle x^1_1,x^2_1,x^2_2,x^3_1,x^3_2,x^3_4,\dots\rangle$$
in $X$. Note that if $1\le k\le m<n$, there is at most one $s\in\{1,\dots,n\}$ such that $d(x^m_k,x^n_s)<\frac{r}2$: this is an easy consequence of the triangle inequality and the fact that the points $x^n_1,\dots,x^n_n$ are mutually at least $r$ apart.
For $n\in\Bbb Z^+$ let $B_n=\{x^n_1,\dots,x^n_n\}$. Let $y_1=x^1_1$. Suppose that $n\in\Bbb Z^+$ and that we’ve chosen $y_k\in B_k$ for $1\le k\le n$ so that the points $y_1,\dots,y_n$ are mutually at least $r/2$ apart. For $k=1,\dots,n$ let $A_k=\varnothing$ if $d(y_k,x)\ge r/2$ for each $x\in B_{n+1}$, and let $A_k=\{x\}$ if $x$ is the unique member of $B_k$ whose distance from $y_k$ is less than $r/2$. Let $A=\bigcup_{k=1}^nA_k$; clearly $|A|\le n$, so $B_{n+1}\setminus A\ne\varnothing$, and we may set $y_{n+1}=x^{n+1}_k$, where $k$ is minimal such that $x^{n+1}_k\notin A$. (Note that this choice of $y_{n+1}$ is well-defined and does not require any part of the axiom of choice.) Then $d(y_{n+1},y_k)\ge r/2$ for $k=1,\dots,n$, and the construction goes through to produce an infinite sequence $\langle y_n:n\in\Bbb Z^+\rangle$ whose terms are mutually at least $r/2$ apart.
But then the set $\{y_n:n\in\Bbb Z^+\}$ is an infinite subset of $X$ with no limit point.