TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

DMC makes every compact Hausdorff space Baire

Statement

$Z F + D M C$ proves that every compact Hausdorff space is a Baire space (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not, Baire space: a topological space in which every countable intersection of dense open subsets is dense).

DMC is the principle of Dependent multiple choice in finite-level tree form, used below in its successor-menu form: every serial relation on a nonempty set admits nonempty finite successor menus.

Facts & Assumptions

Given: A compact Hausdorff space $X$ ; a sequence $(G_{n})_{n \in N}$ of dense open subsets of $X$ ; a nonempty open $W \subseteq X$ ; the principle DMC.

[F1]

A compact Hausdorff space is regular and $T_{1}$ (A compact Hausdorff space is regular and normal, hence $T_{3}$ and $T_{4}$ , Regular spaces and $T_{3}$ spaces, with the source disagreement over whether regularity includes $T_{1}$ stated explicitly, Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

[F2]

Regularity in the shrinking form: if $U$ is open and $x \in U$ then there is open $V$ with $x \in V \subseteq \overline{V} \subseteq U$ (A space is regular if and only if every point has a neighbourhood base of closed neighbourhoods, if and only if $x \in U$ open gives an open $V$ with $x \in V \subseteq \overline{V} \subseteq U$ ).

[F3]

A compact space is countably compact (Countably compact, Lindel"of, sequentially compact, limit point compact and $σ$ -compact spaces, and relatively compact subsets, Compact implies countably compact, Lindel"of and limit point compact; countably compact together with Lindel"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed).

[F4]

DMC: if $R$ is serial on a nonempty set $P$ , there are nonempty finite $F_{n} \subseteq P$ with every $x \in F_{n}$ having an $R$ -successor in $F_{n + 1}$ (Dependent multiple choice in finite-level tree form).

[L1]

Dense means meeting every nonempty open set; an open set is a set whose every point has an open neighbourhood inside it; closures are as in Interior, closure, boundary, exterior, derived set and isolated point in a topological space, and a set is closed exactly when its complement is open (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison, Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L2]

Finite intersections of dense open sets are dense and open, by induction on the number of factors, and finite unions of closed sets are closed (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).

[L3]

A subset of a finite set is finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ); the empty sequence is not used as a menu.

Proof

technique · direct

1.1

Assume DMC. Let $X$ be compact Hausdorff, let $(G_{n})$ be dense open, and let $W$ be nonempty open; if $X = \emptyset$ there is no such $W$ and the Baire condition is vacuous, so assume henceforth $X \neq \emptyset$ .

givenF4

2.1

If $X = \emptyset$ the conclusion of step 1.1 is vacuous: a space with empty underlying set has no nonempty open subset, so every sequence of dense open sets trivially has dense intersection.

step 1.1L1

2.2

Assume $X \neq \emptyset$ ; by [F1] and [F2] $X$ is regular, and by [F3] it is countably compact.

step 1.1F1F2F3

2.3

Put $G_{k}^{'} : = ⋂_{j < k} G_{j}$ for $k \in N$ , so that $G_{0}^{'} = X$ , each $G_{k}^{'}$ is dense and open by [L2], and $G_{k + 1}^{'} \subseteq G_{k}^{'}$ .

step 1.1L2

2.4

Let $V$ be the family of nonempty open subsets of $W$ .

step 1.1L1

3.1

Define $U ≻ V$ for $U, V \in V$ to mean that there is $k$ with $\overline{V} \subseteq U \cap G_{k}^{'}$ and $U \subseteq̸ G_{k}^{'}$ . If some $U \in V$ satisfies $U \subseteq G_{k}^{'}$ for every $k$ , then $U \subseteq W \cap ⋂_{k} G_{k} \neq \emptyset$ and the conclusion already holds; assume therefore that every $U \in V$ fails this, and note that the relation $≻$ is then serial on $V$ : given $U \in V$ , fix $x \in U$ with $x \notin G_{k}^{'}$ for some $k$ , and fix $y \in U \cap G_{k}^{'}$ , which is nonempty because $G_{k}^{'}$ is dense and $U$ is nonempty open; by step 2.2 and [F2] there is nonempty open $V$ with $V \subseteq \overline{V} \subseteq U \cap G_{k}^{'}$ , and $V \subseteq U \subseteq W$ so $V \in V$ and $U ≻ V$ .

step 2.2step 2.3step 2.4F2L1L2

4.1

Assume from now on that the first alternative of step 3.1 fails, so that $≻$ is serial on the nonempty $V$ .

step 3.1

5.1

Apply DMC of [F4] to $≻$ on $V$ : there are nonempty finite sets $V_{n} \subseteq V$ with every $U \in V_{n}$ having a $≻$ -successor in $V_{n + 1}$ .

step 4.1F4

6.1

Prune the menus: put $V_{0}^{'} : = V_{0}$ and $V_{n + 1}^{'} : = {V \in V_{n + 1} : U ≻ V for some U \in V_{n}^{'}}$ . Then each $V_{n}^{'}$ is a nonempty finite subset of $V_{n}$ : nonemptiness is by induction, since each $U \in V_{n}^{'}$ has a $≻$ -successor in $V_{n + 1}$ which then lies in $V_{n + 1}^{'}$ , and finiteness is [L3].

step 5.1L3

7.1

Induction on $n$ : every $U \in V_{n}^{'}$ satisfies $\overline{U} \subseteq G_{n}^{'}$ . For $n = 0$ this is $\overline{U} \subseteq X = G_{0}^{'}$ . For the step, let $V \in V_{n + 1}^{'}$ and fix $U \in V_{n}^{'}$ with $U ≻ V$ ; then $\overline{V} \subseteq U \cap G_{k}^{'}$ for some $k$ with $U \subseteq̸ G_{k}^{'}$ . By the induction hypothesis $U \subseteq \overline{U} \subseteq G_{n}^{'}$ , so $k > n$ : otherwise $G_{k}^{'} \supseteq G_{n}^{'} \supseteq U$ , contradicting $U \subseteq̸ G_{k}^{'}$ . Hence $\overline{V} \subseteq G_{k}^{'} \subseteq G_{n + 1}^{'}$ .

step 3.1step 6.1step 2.3

8.1

Put $W_{n} : = ⋃ V_{n}^{'}$ , a nonempty set with $W_{n} \subseteq G_{n}^{'}$ by step 6.1, and $W_{n + 1} \subseteq W_{n}$ : every $V \in V_{n + 1}^{'}$ satisfies $V \subseteq \overline{V} \subseteq U$ for some $U \in V_{n}^{'} \subseteq W_{n}$ . Put $K_{n} : = ⋃ {\overline{V} : V \in V_{n}^{'}}$ , a nonempty closed set by [L2], with $K_{n + 1} \subseteq W_{n} \subseteq K_{n}$ and $K_{n} \subseteq G_{n}^{'}$ .

step 6.1step 7.1L2

9.1

The sequence $K_{n}$ is a decreasing sequence of nonempty closed subsets of the countably compact space $X$ of step 2.2, so $⋂_{n} K_{n} \neq \emptyset$ : otherwise the open sets $X ∖ K_{n}$ would cover $X$ , and a finite subcover $X ∖ K_{n_{1}}, \dots, X ∖ K_{n_{m}}$ would give $K_{\max n_{j}} = \emptyset$ by [L2], contradicting nonemptiness.

step 2.2step 8.1F3L2

10.1

Fix $x \in ⋂_{n} K_{n}$ ; then $x \in K_{1} \subseteq W_{0} \subseteq W$ by steps 7.1 and 8.1, so $x \in W$ , and for every $n$ we have $x \in K_{n + 1} \subseteq W_{n} \subseteq G_{n}^{'} \subseteq G_{n - 1}$ for $n \geq 1$ , so $x \in ⋂_{n} G_{n}$ ; thus $W \cap ⋂_{n} G_{n} \neq \emptyset$ .

step 8.1step 9.1

11.1

Steps 2.1 and 10.1 cover the empty and nonempty cases of the ambient space, and the only choice principle used was DMC in step 5.1; hence every compact Hausdorff space is Baire.

step 2.1step 10.1F4∎

Remarks

Which hypothesis of the source is used. Fossy and Morillon state the result for countably compact regular spaces; compactness makes the space regular and countably compact in step 2.2, and countable compactness gives the common point of the decreasing closed sets in step 9.1. Hausdorffness is used only through the compact-Hausdorff regularity theorem.
Why the sets $G_{k}^{'}$ are not closed. They are finite intersections of dense open sets, hence dense and open, and they are decreasing; the closed sets whose intersection is taken in step 9.1 are the finite unions of closures of the pruned menus, which is why the pruning of step 6.1 is needed.

Depends on

Used by

Dependency tree · two levels

59 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

David H. Fremlin, Dependent multiple choice and Baire's theorem (following Fossy and Morillon) (standard reference, not scraped)