TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Under Dependent Choice, a nonempty complete metric space is not a countable union of closed sets with empty interior

Statement

Assume the Axiom of Dependent Choice ( $D C$ ). If a nonempty metric space $X$ is complete, then it is not the union of a sequence of closed sets each having empty interior. Equivalently, the intersection of countably many open dense subsets of $X$ is dense.

Facts & Assumptions

Given: The Axiom of Dependent Choice ( $D C$ ), closed sets $F_{1}, F_{2}, \dots \subseteq X$ with empty interior, and a nonempty open set $O \subseteq X$ .

[L1]

A complete metric space contains the limit of every Cauchy sequence (Complete metric space: every Cauchy sequence converges in the space).

[L2]

Under the assumed Axiom of Dependent Choice, a serial sequence of states recording each ball together with its centre and positive radius is permitted (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[L3]

For every positive real number there is a reciprocal integer smaller than it (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Proof

technique · constructive

1.1givenalgebra

If $X$ is empty the assertion is vacuous. Otherwise choose $x_{0} \in O$ and $r_{0} > 0$ such that $\overline{B (x_{0}, r_{0})} \subseteq O$ ; openness supplies a ball about $x_{0}$ in $O$ , and a smaller positive radius has this property. Put $B_{0} = B (x_{0}, r_{0})$ .

1.2givenL3construct

Given $n \geq 1$ and a state $(n - 1, x, r)$ with $r > 0$ , the open set $B (x, r) ∖ F_{n}$ is nonempty because $F_{n}$ is closed with empty interior. Choose $y$ in that set and $s > 0$ small enough that $\overline{B (y, s)} \subseteq B (x, r) ∖ F_{n}$ and $s < 2^{- n}$ ; openness and [L3] permit this for each individual state. Thus the relation from $(n - 1, x, r)$ to $(n, y, s)$ with these properties is serial on the set of triples $(k, z, q) \in N \times X \times (0, \infty)$ .

2.1L2step 1.1step 1.2construct

Apply dependent choice to the serial state relation in step 1.2, starting at $(0, x_{0}, r_{0})$ . Its successive states have first coordinate $n$ , so write them $(n, x_{n}, r_{n})$ and put $B_{n} = B (x_{n}, r_{n})$ . The centres and radii are coordinate projections of this single DC sequence, not separately chosen from countably many balls. They satisfy $x_{n} \in B_{n}$ , $r_{n} < 2^{- n}$ for $n \geq 1$ , and $\overline{B_{n}} \subseteq B_{n - 1} ∖ F_{n}$ .

3.1step 1.2step 2.1L3algebra

The nesting and the radius bound make $(x_{n})$ Cauchy: for $m > n$ , both $x_{m}$ and $x_{n}$ lie in $\overline{B_{n}}$ , so their distance is at most twice the radius of $B_{n}$ , which tends to zero.

4.1L1step 1.2step 3.1algebra

Let $x = \lim_{n} x_{n}$ , supplied by completeness [L1]. For every $n$ , the tail lies in the closed set $\overline{B_{n}}$ , so $x \in \overline{B_{n}} \subseteq B_{n - 1} ∖ F_{n}$ .

5.1step 4.1discharge-construct∎

Thus $x \in O ∖ ⋃_{n} F_{n}$ . Every nonempty open $O$ meets this complement, proving both stated formulations.

Depends on

Dependency tree · 2 levels

Sources

Baire category theorem