TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-05 (gpt-5.6-sol-codex-subscription)‡ rests on unproved material

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.

Assuming dependent choice, every locally compact Hausdorff space is a Baire space

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$ -indexed chain).

Let $(X, \mathcal{T})$ be a locally compact Hausdorff space (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). Then $X$ is a Baire space (Baire space: a topological space in which every countable intersection of dense open subsets is dense): for every sequence $(U_n)_{n \in \mathbb{N}}$ of dense open subsets of $X$ (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure), the intersection $\bigcap_{n \in \mathbb{N}} U_n$ is dense in $X$ .

Dependent choice is sufficient here and no claim of necessity is made. The several statements that go by the name "Baire category theorem" are inequivalent over ZF, and the choice principles they correspond to differ; that account, including the fact that the compact Hausdorff version is equivalent to a principle strictly weaker than dependent choice, is The Baire category theorem is four inequivalent statements over ZF ‡, which this library states and does not prove. Nothing below asserts that dependent choice is needed for the statement above.

Facts & Assumptions

Given: A locally compact Hausdorff space $(X, \mathcal{T})$ , a sequence $(U_n)_{n \in \mathbb{N}}$ of dense open subsets of $X$ , and the Axiom of Dependent Choice.

[L1]

$A \subseteq X$ is dense exactly when $\overline{A} = X$ , exactly when $A$ meets every nonempty open subset of $X$ ; and $X$ is a Baire space when every sequence of dense open sets has dense intersection (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Interior, closure, boundary, exterior, derived set and isolated point in a topological space, Baire space: a topological space in which every countable intersection of dense open subsets is dense).

[L2]

If $O \subseteq X$ is open and $x \in O$ , there is an open $V$ with $x \in V \subseteq \overline{V} \subseteq O$ and $\overline{V}$ a compact subset of $X$ (In a locally compact Hausdorff space every point has a neighbourhood base of compact sets, every open subspace and every closed subspace is locally compact, every open set around a point contains an open set with compact closure inside it, and every compact set sits inside an open set with compact closure, claim 3; Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space).

[L3]

In a Hausdorff space every compact subset is closed (In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, claim 3), and $A \subseteq \overline{A}$ with $\overline{A}$ closed (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L4]

The closed subsets of a subspace are the traces of the closed subsets of the ambient space, and a subset is a compact subset when the subspace it carries is a compact space (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[L5]

A space is compact exactly when every family of its closed subsets with the finite intersection property has nonempty intersection (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection).

[L6]

Assuming dependent choice: if $A$ is nonempty and $(R_n)_{n \in \mathbb{N}}$ are relations on $A$ such that every $u \in A$ has some $v \in A$ with $u \mathbin{R_n} v$ , then for every $a_0 \in A$ there is $a : \mathbb{N} \to A$ with $a(0) = a_0$ and $a(n) \mathbin{R_n} a(n+1)$ for every $n$ (Dependent choice along a sequence of relations: if $R_n$ is entire on $A$ for every $n$ , then from any $a$ there is a sequence with $a_n \mathbin{R_n} a_{n+1}$ , Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure, The natural numbers $\mathbb{N}$ (von Neumann)).

Proof

technique · direct

1.1

By [L1] it suffices to show that every nonempty open $W \subseteq X$ meets $\bigcap_{n \in \mathbb{N}} U_n$ ; if $X$ has no nonempty open subset the requirement is vacuous and there is nothing to prove, so fix a nonempty open $W$ .

L1suffices: every nonempty open W meets the intersection

2.1

$W \cap U_0$ is open and nonempty, $U_0$ being dense and $W$ nonempty open; fixing a point of it, [L2] gives an open $V_0$ with that point in $V_0$ and $\overline{V_0} \subseteq W \cap U_0$ , with $\overline{V_0}$ a compact subset of $X$ . In particular $V_0$ is nonempty.

L1L2step 1.1

3.1

Let $\mathcal{A}$ be the set of nonempty open $V \subseteq X$ whose closure $\overline{V}$ is a compact subset of $X$ ; it contains $V_0$ by step 2.1, so it is nonempty. For $n \in \mathbb{N}$ define a relation $R_n$ on $\mathcal{A}$ by declaring $V \mathbin{R_n} V'$ to hold exactly when $\overline{V'} \subseteq V \cap U_{n+1}$ .

L1step 2.1construct

4.1

Each $R_n$ is entire on $\mathcal{A}$ : given $V \in \mathcal{A}$ , the set $V \cap U_{n+1}$ is open and nonempty, $U_{n+1}$ being dense and $V$ nonempty open, so fixing a point of it and applying [L2] gives an open $V'$ containing that point with $\overline{V'} \subseteq V \cap U_{n+1}$ and $\overline{V'}$ compact; then $V' \in \mathcal{A}$ and $V \mathbin{R_n} V'$ . This is a pure existence statement and selects nothing, which is why dependent choice and nothing stronger is spent below.

L1L2step 3.1

5.1

By [L6] applied to $\mathcal{A}$ , the relations $R_n$ and the point $V_0$ , there is a sequence $(V_n)_{n \in \mathbb{N}}$ in $\mathcal{A}$ with $V_0$ as given and $\overline{V_{n+1}} \subseteq V_n \cap U_{n+1}$ for every $n \in \mathbb{N}$ .

L6step 3.1step 4.1

6.1

The sets $\overline{V_n}$ are nonempty, since $V_n$ is nonempty and $V_n \subseteq \overline{V_n}$ by [L3], and they decrease: $\overline{V_{n+1}} \subseteq V_n \subseteq \overline{V_n}$ by step 5.1 and [L3]. Each is a compact subset of $X$ and hence closed in $X$ by [L3], so each is the trace of a closed set on $\overline{V_0}$ and therefore closed in the subspace $\overline{V_0}$ by [L4].

L3L4step 5.1

7.1

The family $\{\, \overline{V_n} : n \in \mathbb{N} \,\}$ of closed subsets of the compact space $\overline{V_0}$ has the finite intersection property: the intersection of the empty list is $\overline{V_0}$ , which is nonempty, and the intersection of a nonempty finite list is $\overline{V_N}$ for $N$ the greatest of the indices occurring, the sets being decreasing, and that is nonempty. So [L5] gives a point $x \in \bigcap_{n \in \mathbb{N}} \overline{V_n}$ .

L4L5step 6.1

8.1

That point lies in $W \cap \bigcap_{n \in \mathbb{N}} U_n$ : from $x \in \overline{V_0} \subseteq W \cap U_0$ it lies in $W$ and in $U_0$ , and for every $n \in \mathbb{N}$ it lies in $\overline{V_{n+1}} \subseteq V_n \cap U_{n+1} \subseteq U_{n+1}$ , so it lies in $U_m$ for $m = 0$ and for every $m$ of the form $n+1$ , that is in every $U_m$ .

step 2.1step 5.1step 7.1

9.1

So every nonempty open $W$ meets $\bigcap_{n \in \mathbb{N}} U_n$ , which by [L1] makes that intersection dense; as $(U_n)$ was an arbitrary sequence of dense open sets, $X$ is a Baire space.

L1step 1.1step 8.1∎

Remarks

Where each hypothesis is spent. Local compactness and the Hausdorff condition enter only through [L2], the shrinking clause of In a locally compact Hausdorff space every point has a neighbourhood base of compact sets, every open subspace and every closed subspace is locally compact, every open set around a point contains an open set with compact closure inside it, and every compact set sits inside an open set with compact closure, which is used twice: once to start the construction and once to continue it. Compactness of $\overline{V_0}$ is used once, at step 7.1, to turn a decreasing sequence of nonempty closed sets into a common point; that is the finite intersection characterisation A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection and nothing else.

Why the stage-dependent form of dependent choice is needed. The $n$ -th shrinking must land inside $U_{n+1}$ , so the admissible successors of $V$ change with $n$ ; that is a family of relations and not a relation, and The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$ -indexed chain as stated applies to a single relation on a single set. Dependent choice along a sequence of relations: if $R_n$ is entire on $A$ for every $n$ , then from any $a$ there is a sequence with $a_n \mathbin{R_n} a_{n+1}$ is exactly the bridge, and it costs nothing beyond dependent choice itself.

Each $U_n$ is used exactly once. The base step consumes $U_0$ and the step from $V_n$ to $V_{n+1}$ consumes $U_{n+1}$ , so as $n$ ranges over $\mathbb{N}$ every index is consumed and none twice. Since $\mathbb{N}$ contains $0$ , dropping the base step would leave $U_0$ untouched and the conclusion false as stated; the accounting is checked at step 8.1, where membership in $U_m$ is established separately for $m = 0$ and for $m = n+1$ .

Depends on

Used by

The quasicompact convention, why compactness of a subset is read intrinsically here, and what each result on this page costs in choice Remark

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 127 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Baire category theorem (Wikipedia) (standard reference, not scraped)
Locally compact space (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §48 (standard reference, not scraped)
Stacks Project, Section 5.13: Locally quasi-compact spaces (standard reference, not scraped)