4
$\begingroup$

I am studying the book by Brézis on functional analysis and I just read Baire theorem below:

enter image description here

I understood the idea of the proof. My problem is formalizing it. I was trying to deduce the existence of the sequences $(x_n)$ and $(r_n)$ and its properties using recursion, induction and choice. The theorems I have are

Thm. 1 (Recursion): Let $A$ be a set, $a \in A \ $ and $ \ f: A \to A \ $ be a function. Then there exists an unique sequence $ \ b = (b_n) : \mathbb{N} \to A \ $ such that $ \ b_0 = a \ $ and $ \ b_{n+1} = f(b_n) $, $\forall n \in \mathbb{N}$.

Thm. 2 (Induction): Let $ \ K \subset \mathbb{N} \ $ be such that $ \ 0 \in K \ $ and, $ \forall n \in \mathbb{N}$, if $ \ n \in K$, then $ \ n+1 \in K$. Then $ \ K= \mathbb{N}$.

Together with this version of the axiom of choice:

Axiom (of choice): Let $F$ be a set such that $ \ F \neq \varnothing \ $ and $ \ \varnothing \notin F$. Then there exists a choice function $ \ h : F \to \cup F$, ie, $h(P) \in P$, $\forall P \in F$.

I've tried to deduce the existence of a sequence of nonempty sets $ \ (F_n) \in \big[ \wp(X \times \mathbb{R}) \big]^{\mathbb{N}} \ $ using recursion and to extract a sequence $ \ (x_n , r_n) \in F_n \ $, $\forall n \in \mathbb{N}$, using choice. But I was not able to came with a good recursion base function $ \ f : \wp(X \times \mathbb{R}) \to \wp(X \times \mathbb{R})$.

I need hints to find this function or to try another approach. Any help is appreciated. Thanks in advance.

$\endgroup$

2 Answers 2

3
$\begingroup$

I’d use the axiom of dependent choice ($\mathsf{DC}$), a weaker consequence of the axiom of choice. Let

$$\mathscr{X}=\{\langle x,r,n\rangle\in X\times\Bbb R^+\times\Bbb N:\operatorname{cl}B(x,r)\subseteq O_n\}\;,$$

and define a relation $R$ on $\mathscr{X}$ by setting $\langle x,r,n\rangle\mathrel{R}\langle y,s,m\rangle$ iff

  • $m=n+1$,
  • $\operatorname{cl}B(y,s)\subseteq B(x,r)\cap O_m$, and
  • $s<\frac{r}2$.

$\mathsf{DC}$ then gives you a sequence $\big\langle\langle x_k,r_k,k\rangle:k\in\Bbb N\big\rangle$ such that

$$\langle x_k,r_k,k\rangle\mathrel{R}\langle x_{k+1},r_{k+1},k+1\rangle$$

for each $k\in\Bbb N$.

Added: You can adapt this idea to your tools. Let $I=X\times\Bbb R^+\times\Bbb N$, and for each $\langle x,r,n\rangle\in I$ let

$$A(x,r,n)=\left\{\langle y,s,n+1\rangle\in I:s<\frac{r}2\text{ and }\operatorname{cl}B(y,s)\subseteq B(x,r)\cap O_n\right\}\;.$$

Let $\mathscr{A}=\{A(x,r,n):\langle x,r,n\rangle\in I\}$, and let $h$ be a choice function for $\mathscr{A}$. Use $h$ to define a function $f:I\to I$ to which you can apply the recursion theorem to get a suitable sequence $\big\langle\langle x_n,r_n,n\rangle:n\in\Bbb N\big\rangle$.

$\endgroup$
3
  • $\begingroup$ Thanks for the answer, it is very interesting. But I have to do that just with the theorems I stated above and precisely that version of the AC. Do you have some idea? $\endgroup$
    – Gustavo
    Commented Oct 5, 2016 at 19:40
  • $\begingroup$ Maybe I can do that if I study the proof of $ \ ZFC \Rightarrow DC$. Can you suggest me a book so I can find it? $\endgroup$
    – Gustavo
    Commented Oct 5, 2016 at 22:20
  • $\begingroup$ @Gustavo: I was going to make that suggestion, but then I realized that I can’t point you to a useful source. I’ve been busy with other things this afternoon and haven’t had a chance to think about working just from the tools that you’re given, but I do intend to do so later this evening. $\endgroup$ Commented Oct 5, 2016 at 22:43
2
$\begingroup$

What you really need is the Principle of Dependent Choices, meaning that you have to proceed with a countable number of arbitrary choices such that the (n+1)-th choice depends on the n-th choice, say. In fact, the Baire Theorem for Complete Metric Spaces was shown to be equivalent to the Principle of Dependent Choices by Blair in 1979.

Blair, Charles E. (1977), "The Baire category theorem implies the principle of dependent choices.", Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., v. 25 n. 10, pp. 933–934.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .