TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-02

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 recursively specified sequence of balls 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.1

If $X$ is empty the assertion is vacuous. Otherwise choose an open ball $B_{0}$ whose closure lies in $O$ ; this is possible because $O$ is open.

givenalgebra

1.2

Given a nonempty open ball $B_{n - 1}$ , its intersection with $X ∖ F_{n}$ is nonempty because $F_{n}$ has empty interior. Choose an open ball $B_{n}$ with nonempty closure, $\overline{B_{n}} \subseteq B_{n - 1} ∖ F_{n}$ , and radius below $2^{- n}$ .

givenL3construct

2.1

Dependent choice gives balls $B_{n}$ satisfying step 1.2 for every $n$ . Choose centres $x_{n} \in B_{n}$ .

L2step 1.2choose

3.1

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.

step 1.2step 2.1L3algebra

4.1

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}$ .

L1step 1.2step 3.1algebra

5.1

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

step 4.1discharge-construct∎

Depends on

Used by

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Baire category theorem (standard reference, not scraped)