TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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, every Čech-complete space is Baire

Statement

Assume Dependent Choice. Every Čech-complete space is a Baire space.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

A Tychonoff space $X$ is Čech-complete when there is a Hausdorff compactification $(K, i)$ of $X$ (def-compactification-of-a-tychonoff-space) for which $i [X]$ is a $G_{δ}$ subset of $K$ (def-g-delta-and-f-sigma-in-a-topological-space). The definition asks for one compactification; under the ultrafilter lemma and Dependent Choice, thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as $G_{δ}$ subspaces of Hausdorff compactifications).

[F2]

A Hausdorff compactification of a space $X$ is a pair $(K, i)$ in which $K$ is compact (def-compact-space) and Hausdorff (def-hausdorff-space), and $i : X \to K$ is an embedding with dense image (def-homeomorphism-and-open-maps, def-dense-top). We identify $X$ with $i [X]$ only after naming $i$ ; the density condition is a condition on that named image. (A Hausdorff compactification as a dense embedding into a compact Hausdorff space).

[F3]

A function $f : X \to Y$ is an embedding if $f$ is injective and the corestriction $f_{0} : X \to f [X]$ , $f_{0} (x) = f (x)$ , is a homeomorphism onto $f [X]$ carrying the subspace topology inherited from $Y$ (def-subspace-topology-top). (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

[F4]

A subset $A$ of a topological space $X$ is a $G_{δ}$ set of $X$ when there is a sequence $(V_{n})_{n \in N}$ of open subsets of $X$ with $A = ⋂_{n \in N} V_{n} .$ As everywhere in this library $N$ contains $0$ , so the indexing starts at $0$ . ( $G_{δ}$ and $F_{σ}$ subsets of a topological space, agreeing with the real-line notion).

[F5]

For $S \subseteq X$ the subspace topology on $S$ is $T_{S} : = {U \cap S : U \in T}$ , the family of traces on $S$ of the open sets of $X$ ; a subset of $S$ lying in $T_{S}$ is said to be open in $S$ , and relatively open where the ambient space needs emphasis. Choosing a tracing set needs no choice principle, since $U^{'} : = ⋃ {U \in T : U \cap S \subseteq W}$ is a canonical member of $T$ with $U^{'} \cap S = W$ , for each $W \in T_{S}$ . (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).

[F6]

$A \subseteq X$ is dense in $X$ if $\overline{A} = X$ , and this is equivalent to $U \cap A \neq \emptyset$ for every nonempty open $U \subseteq X$ . (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets).

[F7]

A topological space $(X, T)$ is a Baire space when for every sequence $(U_{n})_{n \in N}$ of subsets of $X$ that are open and dense in $X$ (def-dense-top), the intersection $⋂_{n \in N} U_{n}$ is dense in $X$ . (Baire space: a topological space in which every countable intersection of dense open subsets is dense).

[F8]

Let $X$ be a compact (def-compact-space) Hausdorff (def-hausdorff-space) topological space. Then $X$ is regular (def-regular-and-t3-spaces), $X$ is normal, and $X$ is $T_{1}$ , hence $X$ is $T_{3}$ and $T_{4}$ . (A compact Hausdorff space is regular and normal, hence $T_{3}$ and $T_{4}$ ).

[F9]

For a topological space $(X, T)$ the following are equivalent: (a) $X$ is regular (def-regular-and-t3-spaces); (b) for every $x \in X$ and every open $U$ with $x \in U$ there is an open $V$ with $x \in V \subseteq \overline{V} \subseteq U$ ; (c) every point of $X$ has a neighbourhood base consisting of closed neighbourhoods. (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$ ).

[F10]

$\overline{A}$ is closed, contains $A$ , and is contained in every closed $F \subseteq X$ with $A \subseteq F$ ; so it is the smallest closed superset of $A$ , and $A$ is closed if and only if $A = \overline{A}$ . (A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set, claim 2).

[F11]

Call a binary relation $R \subseteq X \times X$ entire on $X$ when for every $x \in X$ there is $y \in X$ with $x R y$ . The Axiom of Dependent Choice is the statement: for every nonempty set $X$ , every relation $R$ entire on $X$ , and every $a \in X$ , there is a sequence $x : N \to X$ with $x_{0} = a$ and $x_{n} R x_{n + 1}$ for every $n \in N$ . (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[F12]

A topological space $(X, T)$ is compact (def-compact-space) if and only if every family $A$ of closed subsets of $X$ with the finite intersection property (def-finite-intersection-property) satisfies $⋂ A \neq \emptyset$ , where $⋂ \emptyset = X$ . No choice principle is used in either direction. (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, claim 1).

Proof

technique · direct

1.1

Let $X$ be Čech-complete; by [F1] fix a Hausdorff compactification $(K, i)$ of $X$ such that $i [X]$ is a $G_{δ}$ subset of $K$ , write $Y : = i [X]$ and let $T_{K}$ be the topology of $K$ , so $K$ is compact Hausdorff and $i : X \to K$ is an embedding by [F2], and by [F4] there is a sequence $(G_{n})_{n \in N}$ of members of $T_{K}$ with $Y = ⋂_{n \in N} G_{n}$ , whence $Y \subseteq G_{n}$ for every $n \in N$ .

givenF1F2F4

1.2

By [F7] the assertion to be proved is that for every sequence $(U_{n})_{n \in N}$ of open dense subsets of $X$ the set $⋂_{n \in N} U_{n}$ is dense in $X$ , and by [F6] that says exactly that $⋂_{n \in N} U_{n}$ meets every nonempty open $V \subseteq X$ ; fix such a sequence $(U_{n})_{n \in N}$ and such a set $V$ , there being nothing to prove when $X$ has no nonempty open subset, in particular when $X = \emptyset$ .

givenF6F7

2.1

By [F3] the corestriction $i_{0} : X \to Y$ is a homeomorphism onto $Y$ with the subspace topology inherited from $K$ , so $i [V]$ and every $i [U_{n}]$ are open in $Y$ and $i [V] \neq \emptyset$ ; each $i [U_{n}]$ is moreover dense in $Y$ , since for nonempty $S$ open in $Y$ the set $i_{0}^{- 1} [S]$ is nonempty and open in $X$ , hence meets $U_{n}$ by [F6], and the image under $i$ of a point of $i_{0}^{- 1} [S] \cap U_{n}$ lies in $S \cap i [U_{n}]$ ; putting $W : = ⋃ {O \in T_{K} : O \cap Y \subseteq i [V]}$ and $W_{n} : = ⋃ {O \in T_{K} : O \cap Y \subseteq i [U_{n}]}$ for $n \in N$ , the canonical tracing construction of [F5] makes these members of $T_{K}$ with $W \cap Y = i [V]$ and $W_{n} \cap Y = i [U_{n}]$ , and since $W_{n}$ is defined by a formula in $n$ rather than selected, the sequence $(W_{n})_{n \in N}$ is obtained with no appeal to countable choice.

step 1.1step 1.2F3F5F6

2.2

The space $K$ is compact Hausdorff by step 1.1, hence regular by [F8], so clause (b) of [F9] holds in $K$ : for every $y \in K$ and every $P \in T_{K}$ with $y \in P$ there is $O \in T_{K}$ with $y \in O \subseteq \overline{O} \subseteq P$ , all closures being taken in $K$ .

step 1.1F8F9

3.1

Since $i [V]$ is nonempty and open in $Y$ and $i [U_{0}]$ is dense in $Y$ , there is a point $y_{0} \in i [V] \cap i [U_{0}] = Y \cap W \cap W_{0}$ , and $y_{0} \in G_{0}$ because $Y \subseteq G_{0}$ ; thus $y_{0}$ lies in the member $W \cap W_{0} \cap G_{0}$ of $T_{K}$ , and the closure form of regularity yields $O_{0} \in T_{K}$ with $y_{0} \in O_{0} \subseteq \overline{O_{0}} \subseteq W \cap W_{0} \cap G_{0}$ , so that $O_{0} \cap Y \neq \emptyset$ .

step 1.1step 2.1step 2.2F6

3.2

Let $S : = {(n, O) : n \in N, O \in T_{K}, O \cap Y \neq \emptyset}$ and let $R$ hold of $((n, O), (m, O^{'}))$ exactly when $m = n + 1$ and $\overline{O^{'}} \subseteq O \cap W_{m} \cap G_{m}$ ; then $R$ is entire on $S$ , for given $(n, O) \in S$ the set $O \cap Y$ is nonempty and open in $Y$ , so the dense set $i [U_{n + 1}] = Y \cap W_{n + 1}$ meets it in a point $y$ , which lies in $G_{n + 1}$ because $Y \subseteq G_{n + 1}$ and hence lies in the member $O \cap W_{n + 1} \cap G_{n + 1}$ of $T_{K}$ , and the closure form of regularity yields $O^{'} \in T_{K}$ with $y \in O^{'} \subseteq \overline{O^{'}} \subseteq O \cap W_{n + 1} \cap G_{n + 1}$ , so that $(n + 1, O^{'}) \in S$ and $(n, O) R (n + 1, O^{'})$ .

step 1.1step 2.1step 2.2F6

4.1

The class $S$ is a set, being a subset of $N \times T_{K}$ , it is nonempty by step 3.1, and $R$ is entire on it by step 3.2, so [F11] applied to $S$ , $R$ and the starting point $(0, O_{0})$ gives a sequence $s : N \to S$ with $s_{0} = (0, O_{0})$ and $s_{n} R s_{n + 1}$ for every $n \in N$ ; since $R$ raises the first coordinate by exactly one, induction on $n$ gives $s_{n} = (n, O_{n})$ for members $O_{n}$ of $T_{K}$ with $O_{n} \cap Y \neq \emptyset$ , and the definition of $R$ gives $\overline{O_{n + 1}} \subseteq O_{n} \cap W_{n + 1} \cap G_{n + 1}$ for every $n \in N$ , while $\overline{O_{0}} \subseteq W \cap W_{0} \cap G_{0}$ by step 3.1.

step 3.1step 3.2F11

5.1

Each $\overline{O_{n}}$ is closed in $K$ and contains the nonempty set $O_{n}$ by [F10], hence is nonempty, and $\overline{O_{n + 1}} \subseteq O_{n} \subseteq \overline{O_{n}}$ by step 4.1 and [F10], so the family ${\overline{O_{n}} : n \in N}$ is decreasing; a nonempty finite subfamily therefore has intersection $\overline{O_{N}} \neq \emptyset$ , where $N$ is the largest index occurring in it, and the empty subfamily has intersection $K \supseteq \overline{O_{0}} \neq \emptyset$ , so the family consists of closed sets and has the finite intersection property, and compactness of $K$ with claim 1 of [F12] produces a point $y \in ⋂_{n \in N} \overline{O_{n}}$ .

step 4.1F10F12

6.1

For every $n \geq 1$ step 4.1 gives $y \in \overline{O_{n}} \subseteq W_{n} \cap G_{n}$ , and $y \in \overline{O_{0}} \subseteq W \cap W_{0} \cap G_{0}$ , so $y \in ⋂_{n \in N} G_{n} = Y$ by step 1.1, and therefore $y \in Y \cap W_{n} = i [U_{n}]$ for every $n \in N$ and $y \in Y \cap W = i [V]$ by step 2.2; as $i$ is injective by [F3], the point $x : = i_{0}^{- 1} (y)$ of $X$ lies in $V$ and in $U_{n}$ for every $n \in N$ .

step 1.1step 2.2step 4.1step 5.1F3

7.1

Thus $⋂_{n \in N} U_{n}$ meets the arbitrary nonempty open set $V$ , so it is dense in $X$ by step 1.2, and $X$ is a Baire space.

step 1.2step 6.1∎

Remarks

The construction has to be run in $K$ , on ambient open sets that MEET $Y$ . It is tempting to build the nested sets inside $X$ itself, or to ask for a nonempty member of $T_{K}$ contained in some $i [U_{n}]$ ; the second is impossible in general, because a Čech-complete space may sit in its compactification with empty interior. Take $K = [0, 1]$ and $Y$ its set of irrational points, which is a $G_{δ}$ in $K$ since $K ∖ Y$ is countable, and take every $U_{n}$ equal to $X$ . A nonempty open subset of $[0, 1]$ contains an interval of positive length and hence a rational point, so no nonempty member of $T_{K}$ is contained in $Y$ , and $Y$ has empty interior in $K$ . What steps 3.1 and 3.2 use instead is that $O \cap Y \neq \emptyset$ , which is preserved because $i [U_{n + 1}]$ is dense in $Y$ and the shrinking is done with the closure form of regularity.
Where the choice principles enter, and where they do not. Dependent Choice is used once, at step 4.1, and it is genuinely needed: the admissible $(n + 1)$ -st open set depends on the $n$ -th, so the family being selected from is not fixed in advance. Nothing else in the proof selects. The sets $W$ and $W_{n}$ are the canonical tracing sets of [F5], so passing from the relatively open $i [U_{n}]$ to an ambient $W_{n}$ for all $n$ at once is a definition rather than a countable choice; the $G_{n}$ arrive as a sequence from [F4]; and the two individual points $y_{0}$ and $y$ are single existential instantiations.
Compact closures are not what the argument needs. Every $\overline{O_{n}}$ is a closed subset of the compact space $K$ , so the intersection at step 5.1 could equally be obtained from the finite intersection property applied inside $\overline{O_{0}}$ . What is load bearing is only that the $\overline{O_{n}}$ are closed in a compact space and decrease, together with $\overline{O_{n}} \subseteq G_{n}$ , which is what forces the limit point into $Y$ rather than into the remainder $K ∖ Y$ .

Depends on

Used by

FALSE: every metrizable space is Čech-complete False statement

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 114 results over 23 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

David Marker, Descriptive Set Theory, §§1–2 (standard reference, not scraped)
Michael Kunzinger, General Topology, §§11.3–11.4 (standard reference, not scraped)
MFF General Topology course summary, §4.3 (standard reference, not scraped)
Jesse Peterson, Real Analysis, §§3.6–3.7 (standard reference, not scraped)