Alphabeta Math
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.

✓ 31 results · all verified · 7 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 24 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Complete Metrizability, Čech-Completeness, and Baire Category

1 · Prerequisites

2 · Summary

Complete metrizability is the topological form of completeness supplied by Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete, while Baire space: a topological space in which every countable intersection of dense open subsets is dense expresses category through countable intersections of dense open sets. Metric completion, compactness, product topology, and the Stone–Čech universal property provide the ambient constructions used to compare complete metrics with Gδ embeddings and Hausdorff compactifications. The stated choice principles remain explicit when compatible metrics, countable families, or nested selections are required.

Nowhere dense, meagre, residual, Polish, Baire sequence, and Čech-complete spaces are developed first. Alexandrov's two implications connect complete metrizability with Gδ subspaces; product metrics and Hilbert-cube embeddings then yield the Polish characterisations. Continued fractions identify Baire sequence space with the irrational line, finite refinements give the Cantor-space surjection theorem, and compactification arguments establish the internal, metric, category, subspace, sum, and product properties of Čech-completeness.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Nowhere dense, meagre, residual, and comeagre subsets of a topological space

Definition

Let X be a topological space and let A⊆X. The set A is nowhere dense when int⁡(A‾)=∅ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space). It is meagre when there is a sequence (Nn)n∈N of nowhere dense subsets of X with A⊆⋃nNn. It is residual, or comeagre, when X∖A is meagre. The empty union shows that ∅ is meagre, including when X=∅.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

The meagre subsets of a topological space form a sigma-ideal

Statement

For every topological space X, the meagre subsets of X contain ∅ and are closed under taking subsets; assuming the Axiom of Countable Choice, they are also closed under countable unions. Countable Choice is what selects one witnessing sequence of nowhere dense sets for each member of the countable family, before the flattening bijection is applied.

Facts & Assumptions

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

[F1]

Let X be a topological space and let A⊆X. The set A is nowhere dense when int⁡(A‾)=∅ (def-interior-closure-boundary-top). It is meagre when there is a sequence (Nn)n∈N of nowhere dense subsets of X with A⊆⋃nNn. It is residual, or comeagre, when X∖A is meagre. The empty union shows that ∅ is meagre, including when X=∅. (Nowhere dense, meagre, residual, and comeagre subsets of a topological space).

[F2]

N×N≈N (def-equinumerous): the plane of pairs of naturals is countably infinite (def-countable). The bijection is exhibited, not merely asserted to exist. Define 2m by recursion on m (thm-recursion) by 20=1 and 2σ(m)=2m+2m, and set J(m,n)=2m⋅σ(n+n),that isJ(m,n)=2m(2n+1). Then J is a bijection from N×N onto N∖{0}, and σ is a bijection from N onto N∖{0}, so σ−1∘J is a bijection N×N→N. What makes J bijective is the decomposition of a nonzero natural into a power of two times an odd number, existence and uniqueness both. (N×N≈N).

[A1]

The Axiom of Countable Choice (ACω) selects one member from each nonempty set in a sequence of sets. It is used below for the sets of nowhere dense covering sequences.

Proof

technique · direct
1.1givenF1

The empty set is meagre, witnessed by the constant sequence of empty nowhere dense sets. If B⊆A and (Nn) witnesses that A is meagre, the same sequence witnesses that B is meagre.

1.2givenF1A1

Let (Am)m∈N be meagre. For each m, let Wm be the nonempty set of sequences (Nm,n)n∈N of nowhere dense subsets of X satisfying Am⊆⋃nNm,n. Apply [A1] once to (Wm) to choose all these sequences simultaneously. This is the only use of Countable Choice.

2.1F1F2step 1.2

Let b:N→N×N be the bijection in [F2], and put Mk=Nb(k). Every Mk is nowhere dense, and ⋃mAm⊆⋃kMk. Thus the countable union is meagre; the empty indexed family has union ∅ as in step 1.1.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 prove the stated sigma-ideal properties under the stated choice hypothesis.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Equivalent forms of the Baire property

Statement

For a topological space X, the following are equivalent: every countable intersection of dense open sets is dense; every countable union of closed sets with empty interior has empty interior; no nonempty open subset is meagre in X; and every residual subset meets every nonempty open set. The equivalence includes the empty space.

Facts & Assumptions

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

[F1]

Let X be a topological space and let A⊆X. The set A is nowhere dense when int⁡(A‾)=∅ (def-interior-closure-boundary-top). It is meagre when there is a sequence (Nn)n∈N of nowhere dense subsets of X with A⊆⋃nNn. It is residual, or comeagre, when X∖A is meagre. The empty union shows that ∅ is meagre, including when X=∅. (Nowhere dense, meagre, residual, and comeagre subsets of a topological space).

[F2]

A topological space (X,T) (def-topological-space) is a Baire space when for every sequence (Un)n∈N of subsets of X that are open and dense in X (def-dense-top, def-sequence-convergence-top, def-natural-numbers), the intersection ⋂n∈NUn is dense in X. (Baire space: a topological space in which every countable intersection of dense open subsets is dense).

[F3]

For all sets X, a and b, X∖(a∪b)=(X∖a)∩(X∖b),X∖(a∩b)=(X∖a)∪(X∖b). Let F be a set with F≠∅. Then { X∖a:a∈F } is a nonempty set and X∖⋃F=⋂{ X∖a:a∈F },X∖⋂F=⋃{ X∖a:a∈F }. (X∖(a∪b)=(X∖a)∩(X∖b) and X∖(a∩b)=(X∖a)∪(X∖b); and for a nonempty set F, X∖⋃F=⋂{ X∖a:a∈F } and X∖⋂F=⋃{ X∖a:a∈F }).

Proof

technique · direct
1.1givenF1F2F3

Apply complements and De Morgan's laws to pass between dense intersections of open sets and unions of closed nowhere dense sets.

2.1step 1.1F1F2F3

Then localise to a nonempty open set to prove equivalence with no nonempty open subset being meagre; keep the empty-space convention visible.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

Open subspaces and residual subspaces of Baire spaces are Baire

Statement

Every open subspace of a Baire space is Baire. Every residual subspace of a Baire space, with its subspace topology, is Baire.

Facts & Assumptions

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

[F1]

For a topological space X, the following are equivalent: every countable intersection of dense open sets is dense; every countable union of closed sets with empty interior has empty interior; no nonempty open subset is meagre in X; and every residual subset meets every nonempty open set. The equivalence includes the empty space. (Equivalent forms of the Baire property).

[F2]

A set is residual when its complement is contained in the union of one sequence of nowhere dense sets (Nowhere dense, meagre, residual, and comeagre subsets of a topological space).

[F3]

Let (X,T) be a topological space (def-topological-space) and let S⊆X. The subspace topology (also relative topology) on S is TS:={ U∩S:U∈T }, the family of traces on S of the open sets of X. The pair (S,TS) is a subspace of X. A subset of S that lies in TS is said to be open in S, and relatively open where the ambient space needs emphasis. (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).

Proof

technique · direct
1.1F1F3given

Let O be open in a Baire space X, and let (Gn) be dense open subsets of O. Put Fn=O∖Gn and Cn=Fn‾X. Each Cn is nowhere dense in X: if a nonempty X-open V lay in Cn, then V would meet O (since Cn⊆O‾), while the nonempty relatively open V∩O would lie in Cn∩O=Fn, contradicting density of Gn in O.

1.2F1F2given

Let Y be residual in X. By [F2], fix one sequence (Nn) of nowhere dense subsets with X∖Y⊆⋃nNn. Since no nonempty open subset of a Baire space is meagre [F1], Y is dense in X.

2.1F1step 1.1

The sets X∖Cn are dense open in X. By the Baire property, their intersection meets every nonempty open subset V of O; a point in that intersection and V lies in every Gn. Thus O is Baire, including the empty case.

2.2F3step 1.2

Let (Gn) be dense open subsets of Y. Put Fn=Y∖Gn and Cn=Fn‾X. Because Y is dense, each Cn is nowhere dense in X: otherwise a nonempty X-open V⊆Cn would meet Y, and the nonempty relatively open V∩Y would lie in Cn∩Y=Fn, contradicting density of Gn in Y.

3.1F1F2F3step 1.2step 2.2

The single interleaved sequence N0,C0,N1,C1,… witnesses that (X∖Y)∪⋃nCn is meagre; forming it requires no countable selection of witnesses. Given a nonempty relatively open W=V∩Y in Y, V is nonempty open in X. By [F1], V is not contained in that meagre set. Any point of V outside it belongs to Y and every Gn, hence to W∩⋂nGn. Therefore Y is Baire.

4.1step 2.1step 3.1∎

Steps 2.1 and 3.1 establish both assertions.

LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

Every open subspace of a completely metrizable space is completely metrizable

Statement

If X is completely metrizable and U⊆X is open, then U is completely metrizable in its subspace topology.

Facts & Assumptions

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

[F1]

Let (X,d) be a metric space (def-metric-space) and let Td be its metric topology (def-metric-topology). Call Td completely metrizable if some metric ρ on X is topologically equivalent to d, that is Tρ=Td (def-equivalent-metrics), and makes (X,ρ) complete (def-complete-metric-space). Then: 1. Homeomorphism invariance. Let (Y,e) be a metric space and let h:X→Y be a bijection (def-injection-surjection-bijection) such that h and h−1 are continuous (def-metric-continuity). If Td is completely metrizable then so is Te. 2. Closed subspaces. If Td is completely metrizable and A⊆X is closed in (X,d), then TdA is completely metrizable, dA being the subspace metric (def-isometry-and-metric-embedding). 3. The property is strictly weaker than completeness. Let P:=(0,∞)⊆R (def-interval) carry d(x,y):=∣x−y∣ (lem-real-line-is-a-metric-space). Then (P,d) is not complete, while ρP(x,y)  :=  ∣x−y∣  +  ∣1x−1y∣ is a complete metric on P with TρP=Td. So Td is completely metrizable although no completeness assumption holds for d itself. Complete metrizability is a condition on the collection of open sets alone: the metric is quantified over and does not survive into the statement. That is exactly what completeness fails to be, and claim 3 shows the two conditions are genuinely different rather than merely stated differently. (Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete).

[F2]

Let (X,d) be a metric space (def-metric-space), let A⊆X be nonempty and let x,y∈X. Then ∣d(x,A)−d(y,A)∣≤d(x,y), with d(⋅,A) the distance to a nonempty set (def-metric-bounded-diameter). Thus the real-valued function u↦d(u,A) changes by at most d(u,v) between u and v: it is 1-Lipschitz. (∣d(x,A)−d(y,A)∣≤d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz).

Proof

technique · direct
1.1givenF1

If U=∅, its unique metric is compatible and complete. Otherwise choose a complete metric ρ on X compatible with its given topology, as allowed by [F1]. Since U is open, it is also ρ-open.

2.1step 1.1F2

If U=X, the restricted metric ρ∣U×U is compatible and complete. Hence assume U is nonempty and proper, and put F=X∖U. Then F is nonempty and ρ-closed. For x∈U, let δ(x)=inf⁡z∈Fρ(x,z). Openness of U gives δ(x)>0, and [F2] gives ∣δ(x)−δ(y)∣≤ρ(x,y).

3.1step 2.1algebra

Define σ(x,y)=ρ(x,y)+∣1/δ(x)−1/δ(y)∣ on U. This is a metric: it is nonnegative and symmetric, vanishes only when x=y because ρ is a metric, and satisfies the triangle inequality by adding those for ρ and absolute value. Also ρ(x,y)≤σ(x,y).

4.1step 2.1step 3.1F2

The metrics σ and ρ∣U×U induce the same topology. Indeed, fix x∈U and ε>0. If ρ(x,y)<δ(x)/2, then δ(y)>δ(x)/2 by [F2], so ∣1/δ(x)−1/δ(y)∣≤2ρ(x,y)/δ(x)2. Thus ρ(x,y)<min⁡{δ(x)/2,ε/(1+2/δ(x)2)} implies σ(x,y)<ε. Conversely σ(x,y)<ε implies ρ(x,y)<ε by step 3.1.

4.2step 1.1step 2.1step 3.1F2

Let (xn) be σ-Cauchy. Then (xn) is ρ-Cauchy and the real sequence (1/δ(xn)) is Cauchy by step 3.1. Completeness of (X,ρ) gives a limit x∈X, and every Cauchy real sequence is bounded, so 1/δ(xn)≤M for some finite M>0 and all n. Hence δ(xn)≥1/M; [F2] and xn→x imply δ(x)≥1/M>0. If x∈F, its distance to F would be zero, so x∈U.

5.1step 1.1step 2.1step 4.1step 4.2∎

Since x∈U and δ(xn)→δ(x)>0, the reciprocal estimate of step 4.1 gives 1/δ(xn)→1/δ(x). Therefore σ(xn,x)→0, proving completeness of σ. Steps 1.1–2.1 cover the empty and whole-space cases, and step 4.1 gives compatibility in the remaining case. Thus U is completely metrizable.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the Axiom of Countable Choice, a countable intersection of completely metrizable subspaces is completely metrizable

Statement

Assume the Axiom of Countable Choice. If (X,d) is metrizable and (Yn)n∈N is a sequence of completely metrizable subspaces of X, then ⋂nYn is completely metrizable.

Facts & Assumptions

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

[F1]

Let (X,d) be a metric space (def-metric-space) and let Td be its metric topology (def-metric-topology). Call Td completely metrizable if some metric ρ on X is topologically equivalent to d, that is Tρ=Td (def-equivalent-metrics), and makes (X,ρ) complete (def-complete-metric-space). Then: 1. Homeomorphism invariance. Let (Y,e) be a metric space and let h:X→Y be a bijection (def-injection-surjection-bijection) such that h and h−1 are continuous (def-metric-continuity). If Td is completely metrizable then so is Te. 2. Closed subspaces. If Td is completely metrizable and A⊆X is closed in (X,d), then TdA is completely metrizable, dA being the subspace metric (def-isometry-and-metric-embedding). 3. The property is strictly weaker than completeness. Let P:=(0,∞)⊆R (def-interval) carry d(x,y):=∣x−y∣ (lem-real-line-is-a-metric-space). Then (P,d) is not complete, while ρP(x,y)  :=  ∣x−y∣  +  ∣1x−1y∣ is a complete metric on P with TρP=Td. So Td is completely metrizable although no completeness assumption holds for d itself. Complete metrizability is a condition on the collection of open sets alone: the metric is quantified over and does not survive into the statement. That is exactly what completeness fails to be, and claim 3 shows the two conditions are genuinely different rather than merely stated differently. (Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete).

[F2]

Let (X,d) be a metric space (def-metric-space) and define, for x,y∈X, d′(x,y):=min⁡{ d(x,y), 1 },d′′(x,y):=d(x,y)1+d(x,y). Both are well defined: d(x,y)≥0 (lem-metric-nonnegativity), so 1+d(x,y)>0 and is invertible, and the minimum of a two-element set of reals exists (lem-finite-set-has-max, def-max-min). Then: 1. d′ and d′′ are metrics on X. 2. d′(x,y)≤1 and d′′(x,y)<1 for all x,y; hence (X,d′) and (X,d′′) are bounded metric spaces (def-metric-bounded-diameter), and if X≠∅ then diam⁡(X)≤1 for both. 3. d′ and d′′ are each uniformly equivalent to d, hence topologically equivalent to it (def-equivalent-metrics, thm-metric-equivalence-hierarchy). Consequently every metric space carries a bounded metric with exactly the same topology, so boundedness cannot be read off the topology alone. (min⁡(d,1) and d/(1+d) are metrics uniformly equivalent to d, so every metric space carries a bounded metric with the same topology).

[F3]

The Axiom of Countable Choice, written ACω, is the following statement. The statement is: for every family (Xn)n∈N of nonempty sets indexed by N there is a function f with domain N such that f(n)∈Xn for every n∈N. Equivalently, every at most countable family of nonempty sets has a choice function. (The Axiom of Countable Choice (ACω)).

[F4]

Let (X,d) be a metric space (def-metric-space) and let p,q∈X with p≠q. Put r:=d(p,q)/2. Then r>0 and B(p,r)∩B(q,r)=∅. Both sets are open (thm-metric-open-set-algebra) and contain p respectively q (def-metric-ball), so every metric space is Hausdorff: distinct points are separated by disjoint open sets (def-metric-topology). (Distinct points of a metric space have disjoint balls around them).

Proof

technique · direct
1.1givenF1F2F4F3

Assume countable choice to select one bounded compatible complete metric on each subspace.

2.1step 1.1F1F2F4

On the intersection, add the ambient bounded metric to a geometrically weighted sum of the selected metrics.

3.1step 2.1F1F4F2

A Cauchy sequence is Cauchy in every coordinate metric; the coordinate limits agree in the Hausdorff ambient metric and lie in every subspace.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the Axiom of Countable Choice, every Gδ subspace of a complete metric space is completely metrizable

Statement

Assume the Axiom of Countable Choice. If (X,d) is a complete metric space and Y⊆X is Gδ in X, then the subspace Y is completely metrizable.

Facts & Assumptions

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

[F1]

Let (X,T) be a topological space (def-topological-space) and let A⊆X. A is a Gδ set of X when there is a sequence (Vn)n∈N of open subsets of X with A=⋂n∈NVn, and an Fσ set of X when there is a sequence (Fn)n∈N of closed subsets of X with A=⋃n∈NFn. (Gδ and Fσ subsets of a topological space, agreeing with the real-line notion).

[F2]

If X is completely metrizable and U⊆X is open, then U is completely metrizable in its subspace topology. (Every open subspace of a completely metrizable space is completely metrizable).

[F3]

Assume the Axiom of Countable Choice. If (X,d) is metrizable and (Yn)n∈N is a sequence of completely metrizable subspaces of X, then ⋂nYn is completely metrizable. (Under the Axiom of Countable Choice, a countable intersection of completely metrizable subspaces is completely metrizable).

Proof

technique · direct
1.1givenF2F1

The empty subspace has its unique compatible complete metric.

2.1step 1.1F3F2

Otherwise write the subspace as a countable intersection of open subspaces.

3.1step 2.1F3F2

Each open subspace is completely metrizable by the reciprocal-distance lemma, and the countable-intersection metric then gives a compatible complete metric on the intersection.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-09 (gpt-6-astra)Open item page →

Under Dependent Choice, every completely metrizable subspace of a metric space is Gδ

Statement

Assume Dependent Choice. If Y is a completely metrizable subspace of a metric space X, then Y is a Gδ subset of X.

Facts & Assumptions

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

[F2]

A Gδ set is a countable intersection of open sets. (Gδ and Fσ subsets of a topological space, agreeing with the real-line notion)

[F3]

Dependent Choice gives a sequence of successive extensions whenever every finite admissible history has an extension. Apply its entire-relation form to the set of those histories, beginning with the empty history. (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain)

[F5]

For each real r>0 there is an integer n≥1 with 1/n<r. (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε)

Proof

technique · direct
1.1givenF4F1F2

The empty subspace is the constant countable intersection of the ambient open set ∅.

2.1step 1.1F1F4

Let ρ be a compatible complete metric on the nonempty subspace Y and let d be the ambient metric. For n≥1 call an ambient open V n-small when V∩Y≠∅, diam⁡d(V)<1/n, and diam⁡ρ(V∩Y)<1/n. Both conditions are imposed, and neither may be dropped: ρ-smallness alone controls distances measured in ρ but says nothing about ambient distances, so it cannot force a point of Y to be near a prescribed ambient point, while ambient smallness alone gives no ρ-control and so cannot invoke completeness of ρ. Every y∈Y lies in some n-small V, because ρ induces the subspace topology, so a ρ-ball of radius below 1/2n about y contains Bd(y,r)∩Y for some r>0, and r may be shrunk below 1/2n. Let Gn be the union of all n-small ambient open sets, an ambient open set containing Y.

3.1

Every x∈⋂n≥1Gn lies in Y‾. [step 2.1, F5] Indeed, given r>0, choose n≥1 with 1/n<r. There is an n-small open V containing x, and some y∈V∩Y. Then d(x,y)<1/n<r. Thus every ambient ball about x meets Y. This uses only finitely many choices for each fixed r, not a selected sequence.

3.2step 2.1F1F4F3

Let x∈Y‾∩⋂n≥1Gn. For each n pick an n-small Vn with x∈Vn and put Wn:=V1∩⋯∩Vn, an ambient open neighbourhood of x with Wn⊆Vn, so diam⁡d(Wn)<1/n and diam⁡ρ(Wn∩Y)<1/n; the Wn decrease. Then pick yn∈Wn∩Y, which is nonempty because x∈Y‾ and Wn is an ambient neighbourhood of x. The selection over n is a recursion whose nth admissible set depends on the previous choices, so it is licensed by the Dependent Choice of [F3]. Since x,yn∈Wn and diam⁡d(Wn)<1/n, the points yn converge to x in d. For m,n≥N both ym and yn lie in WN∩Y, so ρ(ym,yn)<1/N and the sequence is ρ-Cauchy; completeness of ρ gives it a ρ-limit in Y.

4.1

Let y∈Y be the ρ-limit from step 3.2. [step 3.2, F4, F1] The compatible topologies make yn converge to y in the subspace d-metric, hence in X. It also converges to x. If x≠y, disjoint open neighbourhoods from [F4] would both contain every sufficiently late yn, a contradiction. Hence x=y∈Y.

5.1

Therefore Y=⋂n≥1Gn. [step 2.1, step 3.1, step 4.1, F2] Reindexing by n+1 gives a sequence indexed from zero as in [F2], so Y is Gδ in X. The only countable selection is the stated DC use in step 3.2; the empty case was handled in step 1.1. ∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-09 (gpt-6-astra)Open item page →

Alexandrov's theorem, under Dependent Choice: a subspace of a complete metric space is completely metrizable exactly when it is Gδ

Statement

Assume Dependent Choice. For a subspace Y of a complete metric space X, Y is completely metrizable if and only if Y is a Gδ subset of X.

Facts & Assumptions

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

[F1]

Under Countable Choice, if (X,d) is complete and Y⊆X is Gδ in X, then Y is completely metrizable. (Under the Axiom of Countable Choice, every Gδ subspace of a complete metric space is completely metrizable)

[F2]

Assume Dependent Choice. If Y is a completely metrizable subspace of a metric space X, then Y is a Gδ subset of X. (Under Dependent Choice, every completely metrizable subspace of a metric space is Gδ).

[F3]

DC supplies a sequence beginning at any specified point of an entire relation; Countable Choice selects from any given sequence of nonempty sets. (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain, The Axiom of Countable Choice (ACω))

Proof

technique · direct
1.1givenF1F2

The empty subspace satisfies both conditions.

1.2

The assumed DC supplies the Countable Choice needed by [F1]. [given, F3] For any sequence of nonempty sets, take the set of finite lists choosing from its first finitely many members. This set contains the empty list, and the one-term-extension relation is entire. DC starting at the empty list gives nested lists of every finite length; their union is the required choice function. No implication theorem from a later choice page is used.

2.1

Apply [F1] with the given complete ambient metric and the Countable [step 1.2, F1, F2] Choice just derived. For the converse apply [F2] under the given DC; it needs only a compatible complete metric on Y, not completeness of its inherited metric. Thus both implications have their stated hypotheses.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

CorollaryStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

Open and closed subspaces of a completely metrizable space are completely metrizable, and under Dependent Choice so is every Gδ subspace

Statement

Every open or closed subspace of a completely metrizable space is completely metrizable, including the empty subspace. Assuming Dependent Choice, the same holds for every Gδ subspace.

Facts & Assumptions

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

[F1]

If X is completely metrizable and U⊆X is open, then U is completely metrizable in its subspace topology. (Every open subspace of a completely metrizable space is completely metrizable).

[F2]

Assume Dependent Choice. For a subspace Y of a complete metric space X, Y is completely metrizable if and only if Y is a Gδ subset of X. (Alexandrov's theorem, under Dependent Choice: a subspace of a complete metric space is completely metrizable exactly when it is Gδ).

[F3]

If (X,d) is complete and A⊆X is closed, then the subspace metric on A is complete, without a choice axiom. The converse, complete subspace implies closed, requires countable choice and is not used here (Closed subspaces of complete metric spaces are complete; the converse under countable choice).

[F4]

Let (X,d) be a metric space (def-metric-space) and let Td be its metric topology (def-metric-topology). Call Td completely metrizable if some metric ρ on X is topologically equivalent to d, that is Tρ=Td (def-equivalent-metrics), and makes (X,ρ) complete (def-complete-metric-space). Then: 1. Homeomorphism invariance. Let (Y,e) be a metric space and let h:X→Y be a bijection (def-injection-surjection-bijection) such that h and h−1 are continuous (def-metric-continuity). If Td is completely metrizable then so is Te. 2. Closed subspaces. If Td is completely metrizable and A⊆X is closed in (X,d), then TdA is completely metrizable, dA being the subspace metric (def-isometry-and-metric-embedding). 3. The property is strictly weaker than completeness. Let P:=(0,∞)⊆R (def-interval) carry d(x,y):=∣x−y∣ (lem-real-line-is-a-metric-space). Then (P,d) is not complete, while ρP(x,y)  :=  ∣x−y∣  +  ∣1x−1y∣ is a complete metric on P with TρP=Td. So Td is completely metrizable although no completeness assumption holds for d itself. Complete metrizability is a condition on the collection of open sets alone: the metric is quantified over and does not survive into the statement. That is exactly what completeness fails to be, and claim 3 shows the two conditions are genuinely different rather than merely stated differently. (Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete).

Proof

technique · direct
1.1givenF1F3F4

Use the open-subspace lemma directly.

2.1step 1.1F4F3F2

Choose a compatible complete metric for the ambient space; closed subsets are complete for its restriction, while arbitrary Gδ subsets fall under Alexandrov's theorem.

3.1step 2.1F1F3F2

Include the empty subspace.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Under Dependent Choice, every completely metrizable space is Baire

Statement

Assume Dependent Choice. Every completely metrizable space is a Baire space.

Facts & Assumptions

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

[F1]

Let (X,d) be a metric space (def-metric-space) and let Td be its metric topology (def-metric-topology). Call Td completely metrizable if some metric ρ on X is topologically equivalent to d, that is Tρ=Td (def-equivalent-metrics), and makes (X,ρ) complete (def-complete-metric-space). Then: 1. Homeomorphism invariance. Let (Y,e) be a metric space and let h:X→Y be a bijection (def-injection-surjection-bijection) such that h and h−1 are continuous (def-metric-continuity). If Td is completely metrizable then so is Te. 2. Closed subspaces. If Td is completely metrizable and A⊆X is closed in (X,d), then TdA is completely metrizable, dA being the subspace metric (def-isometry-and-metric-embedding). 3. The property is strictly weaker than completeness. Let P:=(0,∞)⊆R (def-interval) carry d(x,y):=∣x−y∣ (lem-real-line-is-a-metric-space). Then (P,d) is not complete, while ρP(x,y)  :=  ∣x−y∣  +  ∣1x−1y∣ is a complete metric on P with TρP=Td. So Td is completely metrizable although no completeness assumption holds for d itself. Complete metrizability is a condition on the collection of open sets alone: the metric is quantified over and does not survive into the statement. That is exactly what completeness fails to be, and claim 3 shows the two conditions are genuinely different rather than merely stated differently. (Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete).

[F2]

Assume the Axiom of Dependent Choice (DC). 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. (Under Dependent Choice, a nonempty complete metric space is not a countable union of closed sets with empty interior).

[F3]

A topological space (X,T) (def-topological-space) is a Baire space when for every sequence (Un)n∈N of subsets of X that are open and dense in X (def-dense-top, def-sequence-convergence-top, def-natural-numbers), the intersection ⋂n∈NUn is dense in X. (Baire space: a topological space in which every countable intersection of dense open subsets is dense).

Proof

technique · direct
1.1givenF1F2

Choose a compatible complete metric using the definition already established by complete remetrisation.

2.1step 1.1F1F2F3

Apply the published complete-metric Baire category theorem [F2] to the whole space with the compatible complete metric of step 1.1, not to its open subspaces: restricting a complete metric to an open subspace need not leave it complete, as (0,1) with the restricted Euclidean metric shows. [F2] already concludes that a countable intersection of dense open subsets of the whole space is dense, which is the Baire property; translate that conclusion back to the topology. The empty space is Baire vacuously.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

The standard weighted metric on a countable product of bounded complete metric spaces is complete

Statement

Let ((Xn,dn))n∈N be complete metric spaces with dn≤1. On ∏nXn, the formula D(x,y)=∑n=0∞2−(n+1)dn(xn,yn) defines a complete metric inducing the product topology. The empty product is the one-point space.

Facts & Assumptions

Given: The complete bounded metric spaces of the statement. No choice principle is assumed: the limits of any supplied coordinate sequences are unique.

[F1]

The product set. Let I be a set and let Xi be a set for each i∈I. The product is ∏i∈IXi  :=  { x:x is a function with domain I and x(i)∈Xi for every i∈I }, and we write xi:=x(i), the i-th coordinate of x. Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For j∈I the j-th projection is πj:∏i∈IXi→Xj,πj(x):=xj.. The product topology TΠ on ∏iXi is the initial topology of the projections: the topology generated by the subbasis {πi−1[U]:i∈I, U∈Ti}. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes ∏i∈IUi with every Ui open in Xi and Ui=Xi for all but finitely many i. (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

[F2]

Let (X,d) be a metric space (def-metric-space). (X,d) is complete if every Cauchy sequence in (X,d) converges to a point of X; a subset A⊆X is called complete when the metric subspace (A,dA) is complete. (Complete metric space: every Cauchy sequence converges in the space).

[F3]

Throughout, R is the complete ordered field (def-real-numbers) and a sequence of reals is a function a:N→R (def-sequence), written (ak); recall that N contains 0. The sequence of partial sums of a sequence (ak) of reals is sn:=∑k<nak, so that s0=0 and sn+1=sn+an; the series ∑ak converges when (sn) converges, and its sum is then that limit. (Series, partial sums, convergence and the sum, divergence, and the tail series).

[F4]

Let r∈R and let rk be the integer power (def-integer-power), so that r0=1 for every r, including r=0. 1. If ∣r∣<1 then the series ∑rk converges (def-series) and ∑k=0∞rk  =  11−r. 2. If ∣r∣≥1 then ∑rk diverges. The series starts at k=0 and its first term is r0=1; in particular ∑k=0∞2−k=2, while the series starting at k=1 sums to 1. Which starting index is meant has to be said, and it is said here. (For ∣r∣<1, ∑k≥0rk=1/(1−r), and for ∣r∣≥1 the series diverges).

Proof

technique · direct
1.1givenF1F3F4

Put wn=2−(n+1). By [F4], ∑n≥0wn=1 and ∑n≥Nwn=2−N. Since 0≤dn(xn,yn)≤1, the partial sums of ∑nwndn(xn,yn) increase and are bounded by 1, so D(x,y) is finite. Symmetry and D(x,x)=0 hold termwise. If D(x,y)=0, every nonnegative summand vanishes; each wn>0, hence dn(xn,yn)=0 for every n, and [F1] gives x=y. Summing each coordinate triangle inequality to a finite index and passing to the limit gives D(x,z)≤D(x,y)+D(y,z). Thus D is a metric on the product, including when that set is empty.

2.1F1F4step 1.1

For each j, the jth nonnegative summand gives dj(xj,yj)≤2j+1D(x,y). Hence every coordinate projection is D-continuous, so every product-open set is D-open by [F1]. Conversely, fix x in the product and ε>0. Choose N with 2−N<ε/2 by [F4]. The finite-coordinate box U={y:dj(xj,yj)<ε/2 for j<N} is product-open and contains x. For y∈U, its first N summands total less than ε/2 because ∑j<Nwj≤1, and its remaining summands total at most 2−N<ε/2. Thus U⊆BD(x,ε). Applying this at each point of a D-open set with a ball contained in that set shows the set is product-open. The topologies coincide.

3.1F1F2F4step 1.1step 2.1

Let (x(m))m≥0 be a D-Cauchy sequence. For every j, the inequality in step 2.1 makes (xj(m))m a dj-Cauchy sequence. Completeness [F2] gives its unique limit xj∈Xj. The rule j↦xj therefore defines one element x of the product by [F1]; no choices of limits are made. Given ε>0, choose N with 2−N<ε/2. For each of the finitely many j<N, coordinate convergence supplies an index mj after which dj(xj(m),xj)<ε/2; take the maximum of these finitely many indices. For all later m, the first N weighted distances total less than ε/2 and the tail is at most 2−N<ε/2. Hence D(x(m),x)<ε, proving completeness.

4.1F1F3step 1.1step 2.1step 3.1

When the index family itself is empty, [F1] gives the unique empty function as its sole product point; the sum has no terms and is zero, giving the one-point complete metric space and its unique topology. If a countable product has no points, metric and topology assertions are vacuous and no Cauchy sequence exists. These conventions also cover empty coordinate spaces without selecting points in them.

5.1step 1.1step 2.1step 3.1step 4.1∎

Steps 1.1–4.1 establish all asserted metric, topology, completeness, and empty-product clauses.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under countable choice, a countable product of completely metrizable spaces is completely metrizable

Statement

Assume the Axiom of Countable Choice. Every countable product of completely metrizable spaces is completely metrizable, including the empty product.

Facts & Assumptions

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

[F1]

Let ((Xn,dn))n∈N be complete metric spaces with dn≤1. On ∏nXn, the formula D(x,y)=∑n=0∞2−(n+1)dn(xn,yn) defines a complete metric inducing the product topology. The empty product is the one-point space. (The standard weighted metric on a countable product of bounded complete metric spaces is complete).

[F2]

Let (X,d) be a metric space (def-metric-space) and define, for x,y∈X, d′(x,y):=min⁡{ d(x,y), 1 },d′′(x,y):=d(x,y)1+d(x,y). Both are well defined: d(x,y)≥0 (lem-metric-nonnegativity), so 1+d(x,y)>0 and is invertible, and the minimum of a two-element set of reals exists (lem-finite-set-has-max, def-max-min). Then: 1. d′ and d′′ are metrics on X. 2. d′(x,y)≤1 and d′′(x,y)<1 for all x,y; hence (X,d′) and (X,d′′) are bounded metric spaces (def-metric-bounded-diameter), and if X≠∅ then diam⁡(X)≤1 for both. 3. d′ and d′′ are each uniformly equivalent to d, hence topologically equivalent to it (def-equivalent-metrics, thm-metric-equivalence-hierarchy). Consequently every metric space carries a bounded metric with exactly the same topology, so boundedness cannot be read off the topology alone. (min⁡(d,1) and d/(1+d) are metrics uniformly equivalent to d, so every metric space carries a bounded metric with the same topology).

[F3]

The Axiom of Countable Choice, written ACω, is the following statement. The statement is: for every family (Xn)n∈N of nonempty sets indexed by N there is a function f with domain N such that f(n)∈Xn for every n∈N. Equivalently, every at most countable family of nonempty sets has a choice function. (The Axiom of Countable Choice (ACω)).

[F4]

Let (X,d) be a metric space (def-metric-space) and let Td be its metric topology (def-metric-topology). Call Td completely metrizable if some metric ρ on X is topologically equivalent to d, that is Tρ=Td (def-equivalent-metrics), and makes (X,ρ) complete (def-complete-metric-space). Then: 1. Homeomorphism invariance. Let (Y,e) be a metric space and let h:X→Y be a bijection (def-injection-surjection-bijection) such that h and h−1 are continuous (def-metric-continuity). If Td is completely metrizable then so is Te. 2. Closed subspaces. If Td is completely metrizable and A⊆X is closed in (X,d), then TdA is completely metrizable, dA being the subspace metric (def-isometry-and-metric-embedding). 3. The property is strictly weaker than completeness. Let P:=(0,∞)⊆R (def-interval) carry d(x,y):=∣x−y∣ (lem-real-line-is-a-metric-space). Then (P,d) is not complete, while ρP(x,y)  :=  ∣x−y∣  +  ∣1x−1y∣ is a complete metric on P with TρP=Td. So Td is completely metrizable although no completeness assumption holds for d itself. Complete metrizability is a condition on the collection of open sets alone: the metric is quantified over and does not survive into the statement. That is exactly what completeness fails to be, and claim 3 shows the two conditions are genuinely different rather than merely stated differently. (Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete).

Proof

technique · direct
1.1givenF4F1F2F3

Use countable choice to select a compatible complete metric in every factor, bound each metric without changing its topology, and invoke the standard weighted product metric.

2.1step 1.1∎

The preceding construction and implications establish the assertion.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Polish spaces are separable completely metrizable spaces

Definition

A topological space is Polish when it is separable (Separability: the existence of an at most countable dense subset) and completely metrizable: its topology is induced by some complete metric (Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete). No particular compatible complete metric or countable dense subset is part of the structure.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

For completely metrizable spaces, the separable and second-countable definitions of Polish space agree under countable choice

Statement

Assume the Axiom of Countable Choice. For a completely metrizable space, separability is equivalent to second countability. Thus either countability convention gives the same notion of Polish space.

Facts & Assumptions

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

[F1]

A topological space is Polish when it is separable (def-separable-space) and completely metrizable: its topology is induced by some complete metric (lem-complete-remetrisation). No particular compatible complete metric or countable dense subset is part of the structure. (Polish spaces are separable completely metrizable spaces).

[F2]

Assuming ACω, a metrizable space is second countable iff it is separable iff it is Lindelöf. (Assuming countable choice, a metrizable space is second countable if and only if it is separable if and only if it is Lindelöf).

Proof

technique · direct
1.1givenF1F2

A completely metrizable space is metrizable.

2.1step 1.1F1F2

Apply the published metrizable-space equivalence between separability and second countability under countable choice, without strengthening the choice claim to ZF.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: AI-adaptedProof: AI-adaptedverified 2026-09-23 (gpt-6-sol)Open item page →

Every separable metrizable space embeds in the Hilbert cube [0,1]N

Statement

Every separable metrizable space is homeomorphic to a subspace of the Hilbert cube [0,1]N.

Facts & Assumptions

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

[F1]

A topological space X is separable if some at most countable subset D⊆X is dense in X (def-dense-top, def-countable). Equivalently, every nonempty open subset of X meets D. (Separability: the existence of an at most countable dense subset).

[F2]

A topological space (X,T) (def-topological-space) is metrizable if there is a metric d on X (def-metric-space) whose metric topology is T, that is T=Td (def-metric-topology). Such a d is said to induce or metrise T. (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

[F3]

The product set. Let I be a set and let Xi be a set for each i∈I. The product is ∏i∈IXi  :=  { x:x is a function with domain I and x(i)∈Xi for every i∈I }, and we write xi:=x(i), the i-th coordinate of x. Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For j∈I the j-th projection is πj:∏i∈IXi→Xj,πj(x):=xj.. The product topology TΠ on ∏iXi is the initial topology of the projections: the topology generated by the subbasis {πi−1[U]:i∈I, U∈Ti}. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes ∏i∈IUi with every Ui open in Xi and Ui=Xi for all but finitely many i. (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

[F4]

Let (X,d) be a metric space (def-metric-space) and define, for x,y∈X, d′(x,y):=min⁡{ d(x,y), 1 },d′′(x,y):=d(x,y)1+d(x,y). Both are well defined: d(x,y)≥0 (lem-metric-nonnegativity), so 1+d(x,y)>0 and is invertible, and the minimum of a two-element set of reals exists (lem-finite-set-has-max, def-max-min). Then: 1. d′ and d′′ are metrics on X. 2. d′(x,y)≤1 and d′′(x,y)<1 for all x,y; hence (X,d′) and (X,d′′) are bounded metric spaces (def-metric-bounded-diameter), and if X≠∅ then diam⁡(X)≤1 for both. 3. d′ and d′′ are each uniformly equivalent to d, hence topologically equivalent to it (def-equivalent-metrics, thm-metric-equivalence-hierarchy). Consequently every metric space carries a bounded metric with exactly the same topology, so boundedness cannot be read off the topology alone. (min⁡(d,1) and d/(1+d) are metrics uniformly equivalent to d, so every metric space carries a bounded metric with the same topology).

Proof

technique · direct
1.1given

The empty space embeds by its unique map into the Hilbert cube. Hence suppose X≠∅.

1.2F1F2F4choose

Choose a metric d inducing the topology of X and put ρ(x,y)=min⁡{d(x,y),1}. By [F4], ρ is a metric with the same topology and values in [0,1]. Choose an at most countable dense set D from [F1]. Since X≠∅, enumerate D as a sequence (an)n∈N, repeating an element if D is finite.

2.1step 1.2F3algebra

Define e:X→[0,1]N by e(x)n=ρ(x,an). For each n, the triangle inequality gives ∣e(x)n−e(y)n∣≤ρ(x,y), so every coordinate is continuous. In the product topology of [F3], inverse images of subbasic coordinate-open sets are therefore open; hence e is continuous.

3.1step 1.2step 2.1F1choose

If x≠y, set δ=ρ(x,y)>0 and choose an with ρ(x,an)<δ/3. The triangle inequality gives e(y)n=ρ(y,an)>2δ/3, while e(x)n<δ/3. Thus e(x)≠e(y) and e is injective.

4.1step 1.2step 2.1step 3.1F1F3algebra

Fix x∈X and ε>0. Choose an with ρ(x,an)<ε/4. The set W={z∈e(X):∣zn−e(x)n∣<ε/2} is open in the subspace e(X) by [F3]. If e(y)∈W, then ρ(y,x)≤ρ(y,an)+ρ(an,x)<ε/2+2ρ(x,an)<ε. Consequently e−1(W)⊆Bρ(x,ε), so the inverse e−1:e(X)→X is continuous at every e(x).

5.1step 1.1step 2.1step 3.1step 4.1∎

Steps 2.1--4.1 make e a homeomorphism of X onto the subspace e(X) of [0,1]N. Together with step 1.1 this covers every separable metrizable space.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under Dependent Choice, a subspace of a Polish space is Polish exactly when it is Gδ

Statement

Assume Dependent Choice, which yields the instances of Countable Choice used below. A subspace of a Polish space is Polish if and only if it is a Gδ subset.

Facts & Assumptions

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

[F1]

A topological space is Polish when it is separable (def-separable-space) and completely metrizable: its topology is induced by some complete metric (lem-complete-remetrisation). No particular compatible complete metric or countable dense subset is part of the structure. (Polish spaces are separable completely metrizable spaces).

[F2]

Assume Dependent Choice. For a subspace Y of a complete metric space X, Y is completely metrizable if and only if Y is a Gδ subset of X. (Alexandrov's theorem, under Dependent Choice: a subspace of a complete metric space is completely metrizable exactly when it is Gδ).

[F3]

Every subspace of a second countable space is second countable. (Second countability is hereditary).

[F4]

Assuming ACω, every second countable space is separable. (Assuming countable choice, every second countable space is separable).

[F5]

Assume the Axiom of Countable Choice. For a completely metrizable space, separability is equivalent to second countability. Thus either countability convention gives the same notion of Polish space. (For completely metrizable spaces, the separable and second-countable definitions of Polish space agree under countable choice).

Proof

technique · direct
1.1givenF2F1F5

Alexandrov gives the complete-metrizability equivalence.

2.1step 1.1F3F4F1

A subspace of a second-countable space is second countable, hence separable under the stated choice hypothesis, while every subspace already inherits metrizability.

3.1step 2.1F3

Combine these facts in both directions.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the Axiom of Choice, a space is Polish exactly when it is homeomorphic to a Gδ subspace of the Hilbert cube

Statement

Assume the Axiom of Choice, which supplies both the Dependent Choice carried by the Polish-subspace characterisation of [F2] and the Choice carried by the Tychonoff theorem of [F4]. A space is Polish if and only if it is homeomorphic to a Gδ subspace of the Hilbert cube [0,1]N.

Facts & Assumptions

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

[F1]

Every separable metrizable space is homeomorphic to a subspace of the Hilbert cube [0,1]N. (Every separable metrizable space embeds in the Hilbert cube [0,1]N).

[F2]

Assume the Axiom of Countable Choice. A subspace of a Polish space is Polish if and only if it is a Gδ subset. (Under Dependent Choice, a subspace of a Polish space is Polish exactly when it is Gδ).

[F3]

Let ((Xn,dn))n∈N be complete metric spaces with dn≤1. On ∏nXn, the formula D(x,y)=∑n=0∞2−(n+1)dn(xn,yn) defines a complete metric inducing the product topology. The empty product is the one-point space. (The standard weighted metric on a countable product of bounded complete metric spaces is complete).

[F4]

Assume the Axiom of Choice (def-axiom-of-choice). Let I be a set and let (Xi,Ti)i∈I be a family of compact topological spaces (def-compact-space, def-topological-space). Then the product P  :=  ∏i∈IXi with the product topology (def-product-topology) is compact. The Axiom of Choice is spent twice, and both uses are flagged below. Once inside thm-alexander-subbase-lemma, through Zorn's lemma (thm-zorn), and once directly at step 2.1, to produce a point of a product of nonempty sets. (Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice).

Proof

technique · direct
1.1givenF1F2F4

Embed a Polish space in the Hilbert cube by universality.

2.1step 1.1F3F1F4

Since the Hilbert cube is complete for its standard product metric, Alexandrov makes the image Gδ.

3.1step 2.1F1F2F4

Conversely, a Gδ subspace of the compact metrizable Hilbert cube is completely metrizable and second countable, hence Polish.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the Axiom of Countable Choice, countable products and Gδ subspaces of Polish spaces are Polish

Statement

Assume the Axiom of Countable Choice. A countable product of Polish spaces is Polish, and every Gδ subspace of a Polish space is Polish.

Facts & Assumptions

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

[F1]

Assume the Axiom of Countable Choice. Every countable product of completely metrizable spaces is completely metrizable, including the empty product. (Under countable choice, a countable product of completely metrizable spaces is completely metrizable).

[F2]

Assuming ACω, a countable product of second countable spaces is second countable. (Assuming countable choice, a countable product of second countable spaces is second countable).

[F3]

Assume the Axiom of Countable Choice. A subspace of a Polish space is Polish if and only if it is a Gδ subset. (Under Dependent Choice, a subspace of a Polish space is Polish exactly when it is Gδ).

[F4]

Assume the Axiom of Countable Choice. For a completely metrizable space, separability is equivalent to second countability. Thus either countability convention gives the same notion of Polish space. (For completely metrizable spaces, the separable and second-countable definitions of Polish space agree under countable choice).

Proof

technique · direct
1.1givenF2F1F4

Use the product theorem for complete metrizability and the published theorem that countable products of second-countable spaces are second countable.

2.1step 1.1F3F4

For a Gδ subspace apply the Polish-subspace characterisation.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Baire sequence space NN and its cylinder topology

Definition

The Baire sequence space is N:=NN, the set of functions from N to itself (The set BA of all functions A→B), with the product topology obtained by giving each copy of N the discrete topology (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies). For a finite sequence s=(s0,…,sk−1), its cylinder is Ns:={x∈N:xi=si for i<k}. The empty sequence has cylinder N, and these cylinders form a basis.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the Axiom of Countable Choice, Baire sequence space is Polish, and its standard ultrametric is complete

Statement

On NN define d(x,y)=0 for x=y and d(x,y)=2−k when k is the least index with xk≠yk. Then d is a complete ultrametric inducing the cylinder topology. Assuming the Axiom of Countable Choice, Baire sequence space is separable and hence Polish.

Facts & Assumptions

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

[F1]

The Baire sequence space is N:=NN, the set of functions from N to itself (def-the-set-of-functions-from-one-set-to-another), with the product topology obtained by giving each copy of N the discrete topology (def-product-topology, def-standard-topologies). For a finite sequence s=(s0,…,sk−1), its cylinder is Ns:={x∈N:xi=si for i<k}. The empty sequence has cylinder N, and these cylinders form a basis. (Baire sequence space NN and its cylinder topology).

[F2]

A topological space is Polish when it is separable (def-separable-space) and completely metrizable: its topology is induced by some complete metric (lem-complete-remetrisation). No particular compatible complete metric or countable dense subset is part of the structure. (Polish spaces are separable completely metrizable spaces).

[F3]

Let (X,d) be a metric space (def-metric-space). (X,d) is complete if every Cauchy sequence in (X,d) converges to a point of X; a subset A⊆X is called complete when the metric subspace (A,dA) is complete. (Complete metric space: every Cauchy sequence converges in the space).

[F4]

Assume the Axiom of Countable Choice. Let (An)n∈N be a family of at most countable sets indexed by N. Then U=⋃n∈NAn is at most countable (Countable unions of at most countable sets, assuming ACω).

Proof

technique · direct
1.1givenF1F3

Give two unequal sequences distance 2−k where k is their first differing index.

2.1step 1.1F1F2

Verify the ultrametric and cylinder topology.

3.1step 2.1F4F1F2

A Cauchy sequence eventually stabilises in every coordinate, producing a limit; eventually constant sequences form a countable dense set.

4.1step 3.1F4

Check the zero-index convention at the first coordinate.

5.1step 4.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-16Open item page →

Under Dependent Choice, every nonempty Polish space is a continuous image of Baire sequence space

Statement

Assume Dependent Choice. Every nonempty Polish space is the image of a continuous surjection from Baire sequence space NN.

Facts & Assumptions

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

[F1]

The Baire sequence space is N:=NN, the set of functions from N to itself (def-the-set-of-functions-from-one-set-to-another), with the product topology obtained by giving each copy of N the discrete topology (def-product-topology, def-standard-topologies). For a finite sequence s=(s0,…,sk−1), its cylinder is Ns:={x∈N:xi=si for i<k}. The empty sequence has cylinder N, and these cylinders form a basis. (Baire sequence space NN and its cylinder topology).

[F2]

A topological space is Polish when it is separable (def-separable-space) and completely metrizable: its topology is induced by some complete metric (lem-complete-remetrisation). No particular compatible complete metric or countable dense subset is part of the structure. (Polish spaces are separable completely metrizable spaces).

[F3]

Let X be a set and let R⊆X×X be a binary relation on X. Call R entire on X when for every x∈X there is y∈X with xRy. The Axiom of Dependent Choice, written DC, is the following statement. The statement is: for every nonempty set X, every relation R entire on X, and every a∈X, there is a sequence x:N→X with x0=a and xnRxn+1 for every n∈N. (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

[F4]

Under Countable Choice for assertion 1, let (X,d) be a metric space (def-metric-space). Call a sequence (Fk)k∈N of subsets of X a Cantor chain if every Fk is nonempty, closed (def-metric-topology) and bounded, Fk+1⊆Fk for every k, and diam⁡(Fk)→0 in R (def-metric-bounded-diameter, def-real-limit). Then: 1. If (X,d) is complete (def-complete-metric-space), every Cantor chain in X has an intersection ⋂k∈NFk with exactly one element. 2. Conversely, if every Cantor chain in X has nonempty intersection, then (X,d) is complete. Boundedness of each Fk is part of the definition of a Cantor chain because diam⁡ is defined for nonempty bounded sets only in this library (def-metric-bounded-diameter); it is not an extra hypothesis but the precondition for writing the diameter condition down. (In a complete metric space nested nonempty closed sets whose diameters tend to 0 meet in exactly one point, and this property characterises completeness).

[F5]

Let (X,d) be a metric space (def-metric-space), let x∈X and let r∈R with r>0 (def-real-order). Define B(x,r):={ y∈X:d(x,y)<r },Bˉ(x,r):={ y∈X:d(x,y)≤r },S(x,r):={ y∈X:d(x,y)=r }. B(x,r) is the open ball, Bˉ(x,r) the closed ball and S(x,r) the sphere of centre x and radius r. The radius is always a strictly positive real; a ball of radius 0 or of negative radius is never written in this library. (Open ball, closed ball and sphere in a metric space).

[F6]

Dependent Choice implies Countable Choice directly: for a sequence (An)n∈N of nonempty sets, let S be the set of finite sequences s with s(i)∈Ai for i<length⁡(s). The empty sequence belongs to S. Relate s to each extension by one entry from Alength⁡(s); this relation is entire because that set is nonempty. Apply [F3] starting at the empty sequence. The resulting nested sequences have lengths 0,1,2,…, and their union is a function choosing an element of every An. No simultaneous choices were used to establish that the relation is entire.

Proof

technique · direct
1.1givenF4F2F5

Choose a compatible complete metric and recursively refine each nonempty open set into a countable cover by open sets whose closures remain inside the parent and whose diameters tend to zero.

2.1step 1.1F1F2F3F4F6

An infinite branch determines one point by completeness. By [F3] and [F6], the Countable Choice hypothesis in [F4] holds, giving a continuous map from Baire space.

3.1step 2.1F3

For a prescribed target point, dependent choice selects a nested branch containing it, proving surjectivity.

4.1step 3.1F4

Nonemptiness is necessary because the domain is nonempty.

5.1step 4.1∎

The preceding construction and implications establish the assertion.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-16Open item page →

Simple continued fractions, convergents, and the integer-coordinate coding of NN

Definition

Define a bijection z:N→Z by z(2k)=k and z(2k+1)=−(k+1); the division algorithm makes these two cases exhaustive (Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b). For x∈NN put a0=z(x0) and an=xn+1 for n≥1. Its finite simple continued fractions [a0;…,an] are defined by recursion on the length, evaluated in Q (The rationals as equivalence classes of pairs of integers, Arithmetic on the rationals): [an]:=an,[ak;ak+1,…,an]:=ak+1[ak+1;…,an](k<n). The recursion never divides by zero, because aj≥1 for j≥1 makes every tail value [ak+1;…,an] at least 1. A finite prefix determines the cylinder of all codes extending it. Infinite continued-fraction values are established, rather than assumed, in Infinite simple continued fractions parametrise the irrational real numbers.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Continued-fraction convergents, determinant identities, and nested irrational cylinders

Statement

Let a0∈Z and an∈Z with an≥1 for n≥1. Define the convergent numerators and denominators by the initial values p−2=0,p−1=1,q−2=1,q−1=0 together with the recurrences pn=anpn−1+pn−2 and qn=anqn−1+qn−2 for n≥0. The initial values are part of the definition: without them the two recurrences have no value at n=0 and n=1. Then p0=a0 and q0=1; the qn are positive for n≥0 and strictly increasing for n≥1; and pnqn−1−pn−1qn=(−1)n−1(n≥0).

For a finite prefix (a0,…,an) write C(a0,…,an)⊆NN for the code cylinder of all codes extending that prefix, and write J(a0,…,an):=the closed interval with endpoints pnqn and pn+pn−1qn+qn−1⊆R. The intervals J are nested as the prefix is extended, and diam⁡J(a0,…,an)=1qn(qn+qn−1), which tends to 0.

A code cylinder and a real interval are different objects and the two are not identified here. Both endpoints of J(a0,…,an) are rational, being ratios of integers. Whether an infinite code's value can equal such an endpoint is not settled on this page; it is settled in Infinite simple continued fractions parametrise the irrational real numbers, which proves every such value irrational.

Facts & Assumptions

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

[F1]

Define a bijection z:N→Z by z(2k)=k and z(2k+1)=−(k+1); the division algorithm makes these two cases exhaustive (thm-division-algorithm-in-z). For x∈NN put a0=z(x0) and an=xn+1 for n≥1. Its finite simple continued fractions are [a0;…,an], evaluated in Q (def-rationals, def-rat-operations). A finite prefix determines the cylinder of all codes extending it. Infinite continued-fraction values are established, rather than assumed, in thm-simple-continued-fractions-parametrise-the-irrationals. (Simple continued fractions, convergents, and the integer-coordinate coding of NN).

[F2]

Let (N,0,σ) be a Peano system (def-peano-system), in particular the natural numbers N (def-natural-numbers). For any set A, any element a∈A, and any function f:A→A, there is a unique function g:N→A such that g(0)=a and g(σ(n))=f(g(n)) for all n∈N. (The recursion theorem).

[F3]

The relation of def-rat-order is well defined and makes the field Q (thm-rat-field) a totally ordered field: the order is total, x≤y implies x+z≤y+z, and 0<x, 0<y imply 0<xy. (The rationals form a totally ordered field).

[F4]

For each k∈N let Ik=[ak,bk] be a closed bounded interval with ak≤bk (def-interval), and suppose the family is nested: Ik+1⊆Ik(k∈N). Write ℓk=bk−ak≥0 for the length of Ik. Then: 1. ⋂k∈NIk is nonempty. More precisely, with a=sup⁡{ak:k∈N} and b=inf⁡{bk:k∈N}, both of which exist, one has a≤b and ⋂k∈NIk=[a,b]. 2. ⋂k∈NIk is a single point if and only if ℓk→0 (def-real-limit). Every hypothesis is load bearing. Dropping closedness makes the intersection empty; dropping boundedness does the same; and dropping nonemptiness of the individual intervals is vacuously fatal. (A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to 0).

[F5]

The map q↦q^ (def-real-numbers) is an embedding of ordered fields. Every real is approximated by rationals: for x∈R and rational ε>0 there is q∈Q with ∣x−q^∣<ε^. Consequently, strictly between any two reals lies a rational. (The rationals embed densely in the reals).

Proof

technique · direct
1.1givenF1F3F5F2

The recursion theorem [F2], applied on pairs, makes (pn,qn)n≥−2 well defined from the four initial values and the two recurrences; p0=a0⋅1+0=a0 and q0=a0⋅0+1=1 follow at once. The determinant identity holds at n=0, where p0q−1−p−1q0=a0⋅0−1⋅1=−1=(−1)−1, and passes from n to n+1 because pn+1qn−pnqn+1=(an+1pn+pn−1)qn−pn(an+1qn+qn−1)=−(pnqn−1−pn−1qn); induction in the ordered field [F3] gives it for every n≥0.

2.1step 1.1F4F1F5

After the arbitrary integer term a0 all partial quotients satisfy an≥1, so from q0=1 and q1=a1≥1 the recurrence gives qn+1=an+1qn+qn−1>qn for n≥1: the denominators are positive and strictly increasing, hence unbounded. Subtracting the two endpoint fractions and using the determinant identity of step 1.1 gives pnqn−pn+pn−1qn+qn−1=pnqn−1−pn−1qnqn(qn+qn−1)=(−1)n−1qn(qn+qn−1), so diam⁡J(a0,…,an)=1/(qn(qn+qn−1))→0. Extending a prefix replaces J by one of the subintervals it determines, so the intervals are nested and [F4] applies to them.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Infinite simple continued fractions parametrise the irrational real numbers

Statement

The continued-fraction coding determined by Simple continued fractions, convergents, and the integer-coordinate coding of NN gives a bijection from the sequences (a0,a1,…) with a0∈Z and an≥1 for n≥1 onto R∖Q. Both the coding map and its inverse are continuous for the cylinder and subspace topologies.

Facts & Assumptions

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

[F1]

Define a bijection z:N→Z by z(2k)=k and z(2k+1)=−(k+1); the division algorithm makes these two cases exhaustive (thm-division-algorithm-in-z). For x∈NN put a0=z(x0) and an=xn+1 for n≥1. Its finite simple continued fractions [a0;…,an] are defined by recursion on the length, evaluated in Q (def-rationals, def-rat-operations): [an]:=an and [ak;ak+1,…,an]:=ak+1/[ak+1;…,an] for k<n. The recursion never divides by zero, because aj≥1 for j≥1 makes every tail value [ak+1;…,an] at least 1. A finite prefix determines the cylinder of all codes extending it. Infinite continued-fraction values are established, rather than assumed, in this item. (Simple continued fractions, convergents, and the integer-coordinate coding of NN).

[F2]

Let a0∈Z and an∈Z with an≥1 for n≥1. With the initial values p−2=0, p−1=1, q−2=1, q−1=0 and the recurrences pn=anpn−1+pn−2, qn=anqn−1+qn−2 for n≥0: p0=a0 and q0=1; the qn are positive for n≥0 and strictly increasing for n≥1; and pnqn−1−pn−1qn=(−1)n−1 for n≥0. For a finite prefix (a0,…,an), C(a0,…,an)⊆NN is the code cylinder of all codes extending that prefix, and J(a0,…,an) is the closed real interval with endpoints pn/qn and (pn+pn−1)/(qn+qn−1). The intervals J are nested as the prefix is extended, and diam⁡J(a0,…,an)=1/(qn(qn+qn−1)), which tends to 0. A code cylinder and a real interval are different objects and the two are not identified. Both endpoints of J(a0,…,an) are rational, being ratios of integers; whether an infinite code's value can equal such an endpoint is not settled there. (Continued-fraction convergents, determinant identities, and nested irrational cylinders).

[F3]

Identify Z with its canonical copy inside R. Then for every real x there is exactly one integer m with m≤x<m+1, written ⌊x⌋ and called the integer part, or floor, of x. Existence is the Archimedean property (thm-of-archimedean) together with the well-ordering of N (thm-well-ordering-principle); uniqueness is the discreteness of Z, no integer lying strictly between m and m+1. (Integer part: for every real x there is exactly one integer m with m≤x<m+1).

[F4]

The map q↦q^ (def-real-numbers) is an embedding of ordered fields. Every real is approximated by rationals: for x∈R and rational ε>0 there is q∈Q with ∣x−q^∣<ε^. Consequently, strictly between any two reals lies a rational. (The rationals embed densely in the reals).

[F5]

For each k∈N let Ik=[ck,dk] be a closed bounded interval with ck≤dk (def-interval), and suppose the family is nested: Ik+1⊆Ik for every k∈N. Write ℓk=dk−ck≥0 for the length of Ik. Then: 1. ⋂k∈NIk is nonempty; more precisely, with c=sup⁡{ck:k∈N} and d=inf⁡{dk:k∈N}, both of which exist, one has c≤d and ⋂k∈NIk=[c,d]. 2. ⋂k∈NIk is a single point if and only if ℓk→0. (A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to 0).

[F6]

The Baire sequence space is N:=NN, the set of functions from N to itself, with the product topology obtained by giving each copy of N the discrete topology (def-product-topology, def-standard-topologies). For a finite sequence s=(s0,…,sk−1), its cylinder is Ns:={x∈N:xi=si for i<k}. The empty sequence has cylinder N, and these cylinders form a basis. (Baire sequence space NN and its cylinder topology).

[F7]

For S⊆X the subspace topology on S is TS:={ U∩S:U∈T }, the family of traces on S of the open sets of X; a subset of S lying in TS is said to be open in 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).

[F8]

For dR(x,y):=∣x−y∣: dR is a metric on R, the open ball is the bounded open interval B(x,r)=(x−r,x+r), and consequently U⊆R is open in the metric topology of dR exactly when for every x∈U there is r>0 with (x−r,x+r)⊆U; this topology is called the usual topology of R. (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded, claims 1 to 3).

Proof

technique · direct
1.1givenF1F6F7

Write A for the set of sequences a=(a0,a1,…) with a0∈Z and an≥1 for n≥1, and for a finite prefix put C(a0,…,an):={ b∈A:bk=ak for k≤n }; by [F1] the assignment x↦a with a0=z(x0) and an=xn+1 for n≥1 is a bijection of N=NN onto A, since z is a bijection of N onto Z and m↦m+1 is a bijection of N onto the integers that are at least 1, and it acts coordinatewise, so it carries the cylinder Ns of [F6] onto the cylinder C(t0,…,tk−1) of the decoded prefix t0=z(s0) and ti=si+1 for 1≤i<k, and every C(a0,…,an) arises from exactly one Ns in this way; give A the topology transported along the bijection, so that the bijection is a homeomorphism and, the Ns being a basis of N by [F6] and their images being exactly the sets C(a0,…,an), those sets are a basis of A, which is the cylinder topology of the Statement, while R∖Q carries the subspace topology of [F7] inherited from R.

1.2givenF2algebra

For a∈A let pn and qn be as in [F2] and, for n≥−1, put Mn(t):=(pnt+pn−1)/(qnt+qn−1); the initial values of [F2] give M−1(t)=(1⋅t+0)/(0⋅t+1)=t for every real t, and for n≥0 and every real t≥1 the denominator satisfies qnt+qn−1>0, since q0t+q−1=t>0 and, for n≥1, qn>0 and qn−1>0 by [F2], so Mn is defined at every real t≥1 when n≥0 and at every real t when n=−1.

1.3givenF2F5

For a∈A the intervals J(a0,…,an) are closed and bounded, are nested as n increases, and satisfy diam⁡J(a0,…,an)=1/(qn(qn+qn−1))→0, all by [F2], so by claims 1 and 2 of [F5] their intersection is a single real, written V(a), and V(a)∈J(a0,…,an) for every n∈N; moreover V(a) is irrational, for suppose V(a)=u/v with u,v integers and v≥1, and note first that the qn are positive for n≥0 and strictly increasing for n≥1 by [F2] and are integers, so q1≥1 and qn+1≥qn+1 give qn≥n for n≥1; for n≥1 both V(a) and the endpoint pn/qn lie in J(a0,…,an), so ∣V(a)−pn/qn∣≤1/(qn(qn+qn−1))<1/qn2 because qn−1>0, and hence ∣uqn−vpn∣=vqn ∣V(a)−pn/qn∣<v/qn; taking n>v makes ∣uqn−vpn∣<1, and it is a nonnegative integer, hence 0, so V(a)=pn/qn for every n>v, which is impossible because the determinant identity of [F2] gives pn+1/qn+1−pn/qn=(pn+1qn−pnqn+1)/(qnqn+1)=(−1)n/(qnqn+1)≠0.

2.1step 1.2F2algebra

For n≥−1 and reals s,t at which Mn is defined, clearing denominators gives Mn(s)−Mn(t)=(s−t)(pnqn−1−pn−1qn)/((qns+qn−1)(qnt+qn−1)), and by [F2] the determinant pnqn−1−pn−1qn equals (−1)n−1 for n≥0 while for n=−1 the initial values give p−1q−2−p−2q−1=1⋅1−0⋅0=1; in every case it is 1 or −1, and the denominators are positive by step 1.2, so Mn is strictly monotone on its domain, strictly increasing when that determinant is 1 and strictly decreasing when it is −1.

2.2step 1.2F2algebra

Fix a∈A and n≥0; the recurrences of [F2] give Mn−1(an)=(pn−1an+pn−2)/(qn−1an+qn−2)=pn/qn and Mn−1(an+1)=(pn−1(an+1)+pn−2)/(qn−1(an+1)+qn−2)=(pn+pn−1)/(qn+qn−1), both arguments lying in the domain found in step 1.2 because an≥1 when n≥1 while M−1 is defined on all of R, so by [F2] the interval J(a0,…,an) is the closed interval with endpoints Mn−1(an) and Mn−1(an+1), both of which are rational by [F2]; the interval is nondegenerate because diam⁡J(a0,…,an)=1/(qn(qn+qn−1))>0, and Mn−1 depends only on a0,…,an−1, since pn−1,pn−2,qn−1,qn−2 do.

2.3step 1.1F3algebra

Let x∈R∖Q and define x0:=x, an:=⌊xn⌋ and xn+1:=1/(xn−an); by induction on n every xn is irrational and xn>1 for n≥1, since given xn irrational [F3] supplies the unique integer an with an≤xn<an+1, so that 0≤xn−an<1 with xn−an≠0 because xn is irrational while an is an integer, whence 0<xn−an<1 and xn+1=1/(xn−an)>1, and xn+1 is irrational because a rational nonzero xn+1 would make xn=an+1/xn+1 rational; consequently an=⌊xn⌋≥1 for n≥1, the recursion never divides by zero, and Φ(x):=(a0,a1,…) is a member of the set A of step 1.1.

2.4step 1.1step 1.3F2F7F8

Let S be open in R∖Q, so S=T∩(R∖Q) for some T open in R by [F7], and let a∈A satisfy V(a)∈S; claim 3 of [F8] gives a real r>0 with (V(a)−r,V(a)+r)⊆T, and the diameters diam⁡J(a0,…,an) tend to 0 by [F2], so some n has diam⁡J(a0,…,an)<r; for every b∈C(a0,…,an) the interval J(b0,…,bn) equals J(a0,…,an), because [F2] computes it from the prefix alone, and both V(b) and V(a) lie in it by step 1.3, so ∣V(b)−V(a)∣<r and V(b)∈T∩(R∖Q)=S; hence every point of the preimage lies in a cylinder contained in it, so that preimage is the union of the cylinders it contains and is open by step 1.1, and the coding map is continuous.

3.1step 1.2step 2.2F2algebra

Fix a∈A and n≥0; subtracting and using the determinant identity of [F2] gives Mn(t)−pn/qn=(qn(pnt+pn−1)−pn(qnt+qn−1))/(qn(qnt+qn−1))=−(pnqn−1−pn−1qn)/(qn(qnt+qn−1))=(−1)n/(qn(qnt+qn−1)) for every real t≥1, and at t=1 the value Mn(1)=(pn+pn−1)/(qn+qn−1) is the endpoint of J(a0,…,an) other than pn/qn identified in step 2.2; for t>1 the two differences Mn(t)−pn/qn and Mn(1)−pn/qn therefore have the same sign (−1)n and satisfy ∣Mn(t)−pn/qn∣<∣Mn(1)−pn/qn∣, because qnt+qn−1>qn+qn−1>0, so Mn(t) lies strictly between the two endpoints of J(a0,…,an) and is neither of them.

3.2step 1.2step 2.3F2algebra

Let x∈R∖Q, let (an) and (xn) be as in step 2.3, and let pn and qn be the convergent numerators and denominators of the code Φ(x); then x=Mn(xn+1) for every n∈N, by induction on n: at n=0 the values p0=a0, q0=1, p−1=1 and q−1=0 of [F2] give M0(x1)=(a0x1+1)/x1=a0+1/x1=a0+(x0−a0)=x because x1=1/(x0−a0), and for the inductive step xn+1=an+1+1/xn+2 with xn+2>1, so multiplying numerator and denominator by xn+2 gives Mn(xn+1)=((an+1pn+pn−1)xn+2+pn)/((an+1qn+qn−1)xn+2+qn)=(pn+1xn+2+pn)/(qn+1xn+2+qn)=Mn+1(xn+2) by the recurrences of [F2]; every denominator here is nonzero, since xn+1>1 and xn+2>1 lie in the domains found in step 1.2.

3.3step 2.1step 2.2

Let a,b∈A with a≠b and let m be the least index with am≠bm; the quantities pm−1,pm−2,qm−1,qm−2 are computed from the common initial segment a0,…,am−1 alone, which is empty when m=0, the four quantities then being the initial values of [F2], so by step 2.2 the codes a and b determine the same function M:=Mm−1, and J(a0,…,am) is the closed interval with endpoints M(am) and M(am+1) while J(b0,…,bm) is the closed interval with endpoints M(bm) and M(bm+1); assume am<bm, which costs nothing by symmetry, so that am+1≤bm as these are integers, and all four arguments lie in the domain of M; if M is strictly increasing there, which is one of the two cases of step 2.1, then J(a0,…,am)=[M(am),M(am+1)] and J(b0,…,bm)=[M(bm),M(bm+1)] with M(am+1)≤M(bm), so the two meet in ∅ when M(am+1)<M(bm) and in {M(bm)} when M(am+1)=M(bm), while if M is strictly decreasing the same computation with the endpoints exchanged gives J(a0,…,am)=[M(am+1),M(am)] and J(b0,…,bm)=[M(bm+1),M(bm)] with M(bm)≤M(am+1), so the two meet in at most the single point M(am+1); in both cases J(a0,…,am)∩J(b0,…,bm) has at most one point, and any such point is an endpoint of both intervals and so is rational by step 2.2.

4.1step 1.3step 2.3step 3.1step 3.2

Let x∈R∖Q and let a:=Φ(x) be the code produced in step 2.3; for every n∈N the tail identity of step 3.2 gives x=Mn(xn+1) with xn+1>1, so step 3.1 places x strictly between the two endpoints of J(a0,…,an) and in particular inside it, whence x∈⋂n∈NJ(a0,…,an), which by step 1.3 is the single point V(a); therefore V(Φ(x))=x, and V maps A onto R∖Q.

4.2step 1.3step 3.3

Let a,b∈A with a≠b and let m be least with am≠bm; by step 1.3 the values V(a) and V(b) are irrational with V(a)∈J(a0,…,am) and V(b)∈J(b0,…,bm), so if V(a)=V(b) then that common value would lie in J(a0,…,am)∩J(b0,…,bm) and hence be rational by step 3.3, a contradiction; therefore V(a)≠V(b) and V is injective.

5.1step 1.1step 1.3step 4.1step 4.2

By step 1.3 the map V sends every member of A to an irrational real, it is surjective onto R∖Q by step 4.1 and injective by step 4.2, so V:A→R∖Q is a bijection, its inverse sends an irrational x to the code Φ(x) of step 2.3, and composing with the coordinatewise bijection of step 1.1 presents it as a bijection defined on NN.

6.1step 1.1step 1.3step 2.2step 3.3step 5.1F2F4F7F8

Let C(a0,…,an) be a cylinder and let x∈V[C(a0,…,an)], say x=V(c) with c∈C(a0,…,an), so that J(c0,…,cn)=J(a0,…,an) is a closed interval [α,β] with α<β rational by step 2.2 and x∈[α,β] irrational by step 1.3, giving α<x<β, and by [F4] there are rationals u,v with α<u<x<v<β; if x′ is irrational with u<x′<v then x′=V(b) for exactly one b∈A by step 5.1 and x′∈J(a0,…,an), and were bk≠ak for some k≤n then, taking m to be the least such index, so that m≤n, the nesting of [F2] would put x′ in J(a0,…,am)∩J(b0,…,bm), which by step 3.3 has at most one point and that point is rational, contradicting irrationality of x′, so b∈C(a0,…,an) and x′∈V[C(a0,…,an)]; consequently the set T:=⋃{ (s,t):s<t rational and (s,t)∩(R∖Q)⊆V[C(a0,…,an)] } is a union of open intervals and so is open in R by [F8], and T∩(R∖Q)=V[C(a0,…,an)], the inclusion from left to right being the defining condition of the union and the reverse holding because the interval (u,v) just produced for the arbitrary point x of the image is one of the united intervals; hence that image is open in R∖Q by [F7], and since every open subset of A is a union of cylinders by step 1.1 and the image of a union is the union of the images, V maps open sets to open sets, which for the bijection of step 5.1 says exactly that its inverse is continuous.

7.1step 2.4step 5.1step 6.1∎

The coding map is a bijection onto R∖Q by step 5.1, it is continuous by step 2.4, and its inverse is continuous by step 6.1, which is the assertion.

Remarks

  • The tail identity is what makes the algorithm invert the coding. Running floors and reciprocals on an irrational x produces a code, but nothing in that recipe by itself says the code's value is x again. The identity x=Mn(xn+1) of step 3.2 says it: the whole of x, not merely an approximation to it, is recovered from the first n+1 partial quotients together with the exact remainder xn+1, and since xn+1>1 the value sits strictly inside the n-th prefix interval. The intersection of those intervals is a single point, so it is x.

  • Irrationality is used twice, and for different purposes. It is what makes the algorithm run forever, since a remainder equal to its own integer part would stop it; and it is what makes prefixes separate, since two prefix intervals of the same length belonging to different codes can share only a rational endpoint. The second use is what gives injectivity and the continuity of the inverse at once.

  • Where the parametrisation fails for rationals. Nothing above extends to a rational target: the algorithm terminates, and the coding map is onto the irrationals only. That is the reason the companion identification is with R∖Q and not with R, and the reason Q cannot be homeomorphic to NN by this route.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Baire sequence space is homeomorphic to the irrational real numbers

Statement

Baire sequence space NN is homeomorphic to the irrational subspace R∖Q.

Facts & Assumptions

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

[F1]

The Baire sequence space is N:=NN, the set of functions from N to itself (def-the-set-of-functions-from-one-set-to-another), with the product topology obtained by giving each copy of N the discrete topology (def-product-topology, def-standard-topologies). For a finite sequence s=(s0,…,sk−1), its cylinder is Ns:={x∈N:xi=si for i<k}. The empty sequence has cylinder N, and these cylinders form a basis. (Baire sequence space NN and its cylinder topology).

[F2]

The continued-fraction coding determined by def-simple-continued-fraction-coding gives a bijection from the sequences (a0,a1,…) with a0∈Z and an≥1 for n≥1 onto R∖Q. Both the coding map and its inverse are continuous for the cylinder and subspace topologies. (Infinite simple continued fractions parametrise the irrational real numbers).

Proof

technique · direct
1.1givenF2F1

Decode the zero-th coordinate by the fixed zigzag bijection with the integers and shift every later natural coordinate by one to obtain positive partial quotients.

2.1step 1.1F2F1

The coordinatewise coding preserves cylinders, and the continued-fraction parametrisation and its inverse therefore give the required homeomorphism.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

LemmaStatement: AI-adaptedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

Under Dependent Choice, a compact metric space carries a finitely branching refining tree of covers of arbitrarily small diameter

Statement

Assume Dependent Choice. If K is a nonempty compact metric space, there is a rooted levelled tree T=⋃n∈NTn with every level Tn finite and nonempty, and nonempty compact sets (Ks)s∈T, such that T0 has one root r with Kr=K, every node has a finite nonempty set of children whose sets cover its set, every child set is contained in its parent set, and diam⁡(Ks)≤2−n for s∈Tn after a harmless rescaling of the metric.

The tree is finitely branching with finite levels; it is not itself a finite set. Since every node has at least one child, induction from the root puts a node at every level, so T=⋃n∈NTn is infinite.

Facts & Assumptions

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

[F1]

Let (X,d) be a metric space (def-metric-space), with open sets as in def-metric-topology and balls as in def-metric-ball. An open cover of (X,d) is a family U of open subsets of X with X=⋃U; a subcover is a subfamily that is itself an open cover; and (X,d) is compact when every open cover of it has a finite subcover. (Open cover, subcover, compact metric space, and compact subset of a metric space).

[F2]

Let (X,d) be a compact metric space (def-metric-compactness, def-metric-space) and let F⊆X be closed in X (def-metric-topology). Then F is a compact subset of X: the metric subspace (F,dF) is a compact metric space (def-isometry-and-metric-embedding). No choice principle is used. (A closed subset of a compact metric space is compact).

[F3]

Let (X,d) be a metric space (def-metric-space) and let A,B⊆X. A is bounded if A=∅ or there are x0∈X and a real r>0 with A⊆B(x0,r); and for nonempty bounded A the diameter diam⁡(A) is the supremum of D(A)={d(a,b):a,b∈A}, diameters being written in this library for nonempty bounded sets only. (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[F4]

Let X be a set and let R⊆X×X be a relation, called entire on X when for every x∈X there is y∈X with xRy. The Axiom of Dependent Choice is the statement: for every nonempty set X, every relation R entire on X, and every a∈X, there is a sequence x:N→X with x0=a and xnRxn+1 for every n∈N (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

Proof

technique · direct
1.1givenF1F3

First the balls B(x,1), x∈K, cover K. Compactness gives finitely many centers covering it, so the triangle inequality bounds all distances in K by one finite real number. Hence D=diam⁡d(K) exists. Replace d by d′=d/max⁡{1,D}; this positive constant rescaling preserves the compact topology and gives diam⁡d′(K)≤1. Use d′ for every ball and diameter below. At stage zero take the single root r with Kr=K, so T0 is finite and nonempty and its diameter bound holds.

2.1step 1.1F2F1F3

Let L be a nonempty compact set and ε>0. The open balls B(x,ε/3) for x∈L form an open cover of L, so by the compactness clause of [F1] finitely many of them, say about x0,…,xm, already cover L. The sets L∩B(xi,ε/3)‾ are then finitely many nonempty-or-discardable subsets of L covering L; each is closed in L and hence compact by [F2], and each has diameter at most 2ε/3<ε by the triangle inequality and the diameter clause of [F3]. Discarding the empty ones leaves a finite nonempty family of nonempty compact subsets of L, covering L, each of diameter below ε.

3.1step 2.1F1F4

Apply step 2.1 with ε=2−(n+1) to every node of level n to obtain that node's children, and let Tn+1 be the resulting finite set of children. Each level is finite because level n is finite and each of its nodes gets finitely many children, and each level is nonempty because every node has at least one child. The passage from one level to the next makes a selection — step 2.1 supplies at least one admissible finite family per node but names none canonically — and the family available at level n+1 is not known until level n is fixed, so the recursion is licensed by Dependent Choice, applied via [F4] to the relation "is an admissible next level for" on finite levelled labellings, taking the root labelling of step 1.1 as the prescribed starting point. This is the Statement's hypothesis and the only place it is used.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-16Open item page →

Under Dependent Choice, every nonempty compact metric space is a continuous image of Cantor space

Statement

Assume Dependent Choice. Every nonempty compact metric space is the image of a continuous surjection from Cantor space {0,1}N.

Facts & Assumptions

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

[F1]

If K is a nonempty compact metric space, there is a rooted levelled tree T=⋃n∈NTn, finitely branching with every level Tn finite and nonempty — so T itself is infinite — and nonempty compact sets (Ks)s∈T such that T0 has one root r with Kr=K, every node has a finite nonempty set of children whose sets cover its set, every child set is contained in its parent set, and diam⁡(Ks)≤2−n for s∈Tn after a harmless rescaling of the metric. (Under Dependent Choice, a compact metric space carries a finitely branching refining tree of covers of arbitrarily small diameter).

[F2]

Let (X,d) be a compact metric space (def-metric-compactness, def-metric-space). Then (X,d) is totally bounded (def-totally-bounded) and complete (def-complete-metric-space). Both implications are theorems of ZF. Completeness is obtained here from the finite intersection characterisation (thm-compact-iff-finite-intersection-property) applied to the closures of the tails of a Cauchy sequence, and not from the extraction of a convergent subsequence, which would route the argument through sequential compactness. What matters for the ledger is that the route taken below selects nothing at all; the first remark below says why the other route was not taken. (A compact metric space is complete and totally bounded, and neither implication uses any choice principle).

[F3]

Under Countable Choice for assertion 1, let (X,d) be a metric space (def-metric-space). Call a sequence (Fk)k∈N of subsets of X a Cantor chain if every Fk is nonempty, closed (def-metric-topology) and bounded, Fk+1⊆Fk for every k, and diam⁡(Fk)→0 in R (def-metric-bounded-diameter, def-real-limit). Then: 1. If (X,d) is complete (def-complete-metric-space), every Cantor chain in X has an intersection ⋂k∈NFk with exactly one element. 2. Conversely, if every Cantor chain in X has nonempty intersection, then (X,d) is complete. Boundedness of each Fk is part of the definition of a Cantor chain because diam⁡ is defined for nonempty bounded sets only in this library (def-metric-bounded-diameter); it is not an extra hypothesis but the precondition for writing the diameter condition down. (In a complete metric space nested nonempty closed sets whose diameters tend to 0 meet in exactly one point, and this property characterises completeness).

[F4]

The product set. Let I be a set and let Xi be a set for each i∈I. The product is ∏i∈IXi  :=  { x:x is a function with domain I and x(i)∈Xi for every i∈I }, and we write xi:=x(i), the i-th coordinate of x. Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For j∈I the j-th projection is πj:∏i∈IXi→Xj,πj(x):=xj.. The product topology TΠ on ∏iXi is the initial topology of the projections: the topology generated by the subbasis {πi−1[U]:i∈I, U∈Ti}. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes ∏i∈IUi with every Ui open in Xi and Ui=Xi for all but finitely many i. (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

[F5]

Throughout, a topology is as in def-topological-space, and finite, at most countable and uncountable are as in def-countable, so that "countable" always means "at most countable" and every finite set is countable. Let X be a set. The six families below are topologies on X; that each really satisfies (T1), (T2) and (T3) is discharged in full after the list. Among those six is the discrete topology Tdisc:=P(X), in which every subset is open and hence every subset is also closed. (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).

[F6]

Let X be a set and let R⊆X×X be a binary relation on X. Call R entire on X when for every x∈X there is y∈X with xRy. The Axiom of Dependent Choice, written DC, is the following statement. The statement is: for every nonempty set X, every relation R entire on X, and every a∈X, there is a sequence x:N→X with x0=a and xnRxn+1 for every n∈N. (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

[F7]

Dependent Choice implies Countable Choice directly: for a sequence (An)n∈N of nonempty sets, let S be the set of finite sequences s with s(i)∈Ai for i<length⁡(s). The empty sequence belongs to S. Relate s to each extension by one entry from Alength⁡(s); this relation is entire because that set is nonempty. Apply [F6] starting at the empty sequence. The resulting nested sequences have lengths 0,1,2,…, and their union is a function choosing an element of every An. No simultaneous choices were used to establish that the relation is entire.

Proof

technique · direct
1.1givenF1F5F3F4F6

Use the finite rooted refining tree and choose a finite block of binary digits at each level that surjects onto every child set of every node at that level.

2.1step 1.1F2F3F1F6F7

Successive blocks select a nested branch. By [F6] and [F7], the Countable Choice hypothesis in [F3] holds, so the complete compact intersection theorem gives the branch's unique point.

3.1step 2.1F3F2F1

The resulting map from Cantor space is continuous by the diameter bound and surjective by recursively selecting a child containing a prescribed point.

4.1step 3.1F3F2F1

Keep nonemptiness explicit; no map from nonempty Cantor space can surject onto the empty space.

5.1step 4.1∎

The preceding construction and implications establish the assertion.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-16Open item page →

Čech-complete spaces as Gδ subspaces of Hausdorff compactifications

Definition

A Tychonoff space X is Čech-complete when there is a Hausdorff compactification (K,i) of X (A Hausdorff compactification as a dense embedding into a compact Hausdorff space) for which i[X] is a Gδ subset of K (Gδ and Fσ subsets of a topological space, agreeing with the real-line notion). The definition asks for one compactification; under the ultrafilter lemma and Dependent Choice, Under the ultrafilter lemma and Dependent Choice, a Tychonoff space is Gδ in some Hausdorff compactification exactly when it is Gδ in every one proves the equivalent every-compactification form.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

A map of Hausdorff compactifications carries the larger remainder onto the smaller remainder

Statement

Let (K,i) and (L,j) be Hausdorff compactifications of X, and let f:K→L be continuous with f∘i=j. Then f is surjective and f[K∖i[X]]=L∖j[X]. The embeddings are named because the identification of X with its image is licensed only after naming them.

Facts & Assumptions

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

[F1]

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→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).

[F2]

Let (X,TX) and (Y,TY) be topological spaces (def-topological-space), and let R carry its usual topology, the metric topology of dR(s,t)=∣s−t∣ (lem-real-line-is-a-metric-space, def-metric-topology, def-metrizable-space). Then: 1. Continuous images. If f:X→Y is continuous (def-continuous-map-top) and (X,TX) is compact (def-compact-space), then f[X] is a compact subset of Y. More generally, if K⊆X is a compact subset of X then f[K] is a compact subset of Y. 2. Extreme values. If (X,TX) is compact and nonempty and g:X→R is continuous, then g[X] has a maximum and a minimum (def-max-min): there are xmax⁡,xmin⁡∈X with g(xmin⁡)  ≤  g(x)  ≤  g(xmax⁡)for every x∈X. 3. Compact to Hausdorff. If (X,TX) is compact, (Y,TY) is Hausdorff (def-hausdorff-space) and f:X→Y is a continuous bijection, then f is a homeomorphism (def-homeomorphism-and-open-maps). Nonemptiness in claim 2 is a hypothesis and not an oversight: for X=∅ the image is empty and has neither a maximum nor a minimum. No choice principle is used: the one selection made below is over a finite index set, where lem-finite-choice is a theorem of ZF. (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[F3]

Let (X,T) be a Hausdorff topological space (def-hausdorff-space, def-topological-space), with compact subsets as in def-compact-space. Then: 1. A point and a disjoint compact set are separated. If K⊆X is compact and x∈X∖K, there are U,V∈T with x∈U,K⊆V,U∩V=∅. 2. Two disjoint compact sets are separated. If K,L⊆X are compact and K∩L=∅, there are U,V∈T with L⊆U,K⊆V,U∩V=∅. 3. Compact implies closed. Every compact subset of X is closed in X. 4. In a compact Hausdorff space the two classes coincide. If in addition (X,T) is compact, then a subset of X is compact if and only if it is closed. The proof is written choice-free, and that is not a stylistic preference. The textbook argument says "for each y∈K choose disjoint open Uy,Vy", which is a selection over an arbitrary index set and therefore an appeal to the full Axiom of Choice. What is done below instead is to take the family of all open V that admit some open U∋x disjoint from them — a family cut out by a formula, with nothing selected — extract a finite subcover from it, and only then make finitely many selections, which lem-finite-choice supplies as a theorem of ZF. (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).

Proof

technique · direct
1.1givenF2F1F3

Let a continuous map between compactifications restrict to the identity on the dense copy of the space.

2.1step 1.1F3F1F2

Compactness makes its image closed and density makes it surjective.

3.1step 2.1F3F1F2

If a remainder point mapped into the dense copy, Hausdorff separation and density would contradict identity on the copy; conversely compactness of a fibre over a remainder point supplies a preimage outside the copy.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the ultrafilter lemma and Dependent Choice, a Tychonoff space is Gδ in some Hausdorff compactification exactly when it is Gδ in every one

Statement

Assume the ultrafilter lemma and Dependent Choice, the hypotheses under which the library establishes the Stone-Čech compactification and its universal property. A Tychonoff space is a Gδ subset of some Hausdorff compactification if and only if it is a Gδ subset of every Hausdorff compactification.

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; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as Gδ subspaces of Hausdorff compactifications).

[F2]

Let X be dense in Hausdorff compactifications K and L, and let f:K→L be continuous with f∣X=id⁡X. Then f is surjective and f[K∖X]=L∖X. (A map of Hausdorff compactifications carries the larger remainder onto the smaller remainder).

[F3]

A Stone–Čech compactification of X is a Hausdorff compactification (B,i) (def-compactification-of-a-tychonoff-space) such that for every compact Hausdorff space K and continuous map f:X→K (def-continuous-map-top), there is a unique continuous fˉ:B→K with fˉ∘i=f. The universal property, rather than a particular construction, is the definition. (The Stone–Čech compactification by its compact-Hausdorff extension property).

[F4]

Under the hypotheses of thm-stone-cech-evaluation-closure-universal-property, two Stone–Čech compactifications (B,i) and (B′,i′) of X are uniquely homeomorphic by a map u:B→B′ satisfying u∘i=i′. (Stone–Čech compactifications are uniquely homeomorphic over the original space).

Proof

technique · direct
1.1givenF1F3F4

For the empty space the empty compactification witnesses both quantifiers.

2.1step 1.1F3F1F4

Otherwise use the Stone–Čech compactification as a common dominating compactification.

3.1step 2.1F1F2F3

The remainder-map lemma transfers the compact Fσ remainder condition along the canonical maps, and complements convert it back to the Gδ condition.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the ultrafilter lemma, Frolík's internal open-cover characterisation of Čech-completeness

Statement

Assume the ultrafilter lemma and Dependent Choice, the hypotheses carried by the compactification-independence theorem this proof uses. A Tychonoff space X is Čech-complete if and only if there is a sequence (Un) of open covers of X such that every centred family of closed subsets of X which is subordinate to every Un has nonempty intersection.

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; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as Gδ subspaces of Hausdorff compactifications).

[F2]

Assume the ultrafilter lemma and Dependent Choice. A Tychonoff space is a Gδ subset of some Hausdorff compactification if and only if it is a Gδ subset of every Hausdorff compactification. (Under the ultrafilter lemma and Dependent Choice, a Tychonoff space is Gδ in some Hausdorff compactification exactly when it is Gδ in every one).

[F3]

Let (X,T) be a topological space (def-topological-space). For a family A of subsets of X write ⋂A  :=  { x∈X:x∈A for every A∈A }, so that ⋂∅=X, matching the convention for the empty finite intersection in def-finite-intersection-property. Then: 1. (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≠∅. 2. Equivalently: (X,T) is compact if and only if every family of closed subsets of X that is contained in some filter on X (def-filter) has nonempty intersection, a family of subsets of X lying in a filter exactly when it has the finite intersection property (lem-fip-generates-filter). No choice principle is used in either direction: complementation is a canonical bijection, so no member of a family ever has to be selected. (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection).

[F4]

Let (X,T) be a topological space (def-topological-space). The following implications hold, and each is proved by an earlier item of this page. 1. Perfectly normal implies completely normal, assuming the Axiom of Countable Choice (def-countable-choice). 2. Completely normal implies normal, and perfectly normal implies normal. 3. Normal together with T1 implies T3, that is regular together with T1. 4. Completely regular implies regular, and Tychonoff implies T3. 5. Regular together with T1 implies Urysohn, which implies Hausdorff, which implies T1, which implies T0. 6. Metrizable implies every property named above: a metrizable space is perfectly normal, completely normal, normal, Tychonoff, completely regular, T3, regular, Urysohn, Hausdorff, T1 and T0, with no choice principle used. Reading the numbered axioms in order, clauses 1 to 5 give T6⇒T5⇒T4⇒T3⇒T212⇒T2⇒T1⇒T0, the first arrow under ACω, together with T312⇒T3. This is the whole of the classical chain that this page proves, and it is one arrow short of the classical chain. The implication T4⇒T312 — a normal T1 space is completely regular — is Urysohn's lemma and is not available at this point in the reading order. Its absence is recorded, with what would license it, in this page's conventions remark; it is deliberately not asserted here, and no clause above may be read as giving it. (The implications proved on this page: perfectly normal gives completely normal under countable choice, and completely normal gives normal; normal with T1 gives T3; completely regular gives regular; regular with T1 gives Urysohn, hence Hausdorff, hence T1, hence T0; and metrizable gives every one of them).

[F5]

Let X be a set. A family B⊆P(X) is a filter base on X when it satisfies: - (B1) nonemptiness: B≠∅; - (B2) properness: ∅∉B; - (B3) downward directedness: for all B1,B2∈B there is B3∈B with B3⊆B1∩B2. (Filter base and the filter it generates).

[F6]

Let X be a compact Hausdorff topological space. Then X is regular, and X is normal (A compact Hausdorff space is regular and normal, hence T3 and T4).

Proof

technique · direct
1.1givenF1F2F3F6

From a Gδ presentation in a compactification, use regularity of the compactification to choose open covers whose ambient closures lie in the successive layers. The compactification is compact Hausdorff, so [F6] supplies exactly that regularity; [F4] is the separation chain and does not state the compact-Hausdorff-to-regular implication.

2.1step 1.1F3F4F1

A centred family subordinate to every cover has centred ambient closures, hence a compactness cluster point; the layer condition puts that point back in the original space and closedness puts it in every family member.

3.1step 2.1F3F4F5

Conversely, apply the centred-family condition to neighbourhood traces of each remainder point to construct countably many ambient open sets whose intersection excludes the whole remainder.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the ultrafilter lemma and the Axiom of Choice, every completely metrizable space is Čech-complete

Statement

Assume the ultrafilter lemma and the Axiom of Choice. Every completely metrizable space is Čech-complete.

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; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as Gδ subspaces of Hausdorff compactifications).

[F2]

Let (X,d) be a metric space (def-metric-space) and let Td be its metric topology (def-metric-topology). Call Td completely metrizable if some metric ρ on X is topologically equivalent to d, that is Tρ=Td (def-equivalent-metrics), and makes (X,ρ) complete (def-complete-metric-space). Then: 1. Homeomorphism invariance. Let (Y,e) be a metric space and let h:X→Y be a bijection (def-injection-surjection-bijection) such that h and h−1 are continuous (def-metric-continuity). If Td is completely metrizable then so is Te. 2. Closed subspaces. If Td is completely metrizable and A⊆X is closed in (X,d), then TdA is completely metrizable, dA being the subspace metric (def-isometry-and-metric-embedding). 3. The property is strictly weaker than completeness. Let P:=(0,∞)⊆R (def-interval) carry d(x,y):=∣x−y∣ (lem-real-line-is-a-metric-space). Then (P,d) is not complete, while ρP(x,y)  :=  ∣x−y∣  +  ∣1x−1y∣ is a complete metric on P with TρP=Td. So Td is completely metrizable although no completeness assumption holds for d itself. Complete metrizability is a condition on the collection of open sets alone: the metric is quantified over and does not survive into the statement. That is exactly what completeness fails to be, and claim 3 shows the two conditions are genuinely different rather than merely stated differently. (Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete).

[F3]

Assume the Axiom of Choice. Every metric space is paracompact. (Stone's theorem, under choice: every metric space is paracompact).

[F4]

Consequently every metrizable space (def-metrizable-space) is Tychonoff and perfectly normal, and hence T6, T5, T4, T312, T3, T212, T2, T1 and T0. (In a metric space every closed set is a zero set and a Gδ, and the distance function separates a point from a closed set, so every metrizable space is Tychonoff and perfectly normal).

[F5]

Assume the ultrafilter lemma. If X is Tychonoff, e:X→[0,1]C(X,[0,1]) is its full evaluation map, and K=e[X]‾, then (K,e) is a Hausdorff compactification of X. In particular every Tychonoff space has one. This statement uses the ultrafilter lemma only for compactness of the cube; it makes no assertion about dependent choice. (Assuming the ultrafilter lemma, every Tychonoff space has a Hausdorff compactification).

[F6]

Assume the ultrafilter lemma. A Tychonoff space is a Gδ subset of some Hausdorff compactification if and only if it is a Gδ subset of every Hausdorff compactification. (Under the ultrafilter lemma and Dependent Choice, a Tychonoff space is Gδ in some Hausdorff compactification exactly when it is Gδ in every one).

Proof

technique · direct
1.1givenF1F6F2

The empty space is Gδ in its empty compactification.

2.1step 1.1F2F1F3

Otherwise choose a compatible complete metric and locally finite refinements of the covers by balls of radius tending to zero.

3.1step 2.1F1F2F6F4

In a Hausdorff compactification, extend the refined members to ambient open sets and use local finiteness to form open neighbourhoods whose intersection is exactly the original space: a point in every neighbourhood produces a Cauchy filter and hence a limit in the complete space.

4.1step 3.1F1F6F5

Invoke compactification independence only after this construction is established.

5.1step 4.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the ultrafilter lemma, every metrizable Čech-complete space is completely metrizable

Statement

Assume the ultrafilter lemma, Dependent Choice and Countable Choice — the hypotheses carried by the compactification-independence theorem of [F2] and the completely-metrizable characterisation of [F5]. Every metrizable Čech-complete space is completely metrizable.

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; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as Gδ subspaces of Hausdorff compactifications).

[F2]

Assume the ultrafilter lemma and Dependent Choice. A Tychonoff space is a Gδ subset of some Hausdorff compactification if and only if it is a Gδ subset of every Hausdorff compactification. (Under the ultrafilter lemma and Dependent Choice, a Tychonoff space is Gδ in some Hausdorff compactification exactly when it is Gδ in every one).

[F3]

Let (X,d) be a metric space (def-metric-space) and let C be the set of all Cauchy sequences in X (def-cauchy-in-metric). Then: 1. For all x=(xn) and y=(yn) in C the real sequence (d(xn,yn))n converges, so ρ(x,y)  :=  lim⁡nd(xn,yn) is a single well-determined real (thm-cauchy-criterion-via-lub, lem-limit-unique). 2. The relation x∼y:⟺ρ(x,y)=0 is an equivalence relation on C. Write X^:=C/ ⁣∼ for the set of its classes and [x] for the class of x. 3. d^([x],[y]):=ρ(x,y) does not depend on the chosen representatives, and d^ is a metric on X^. 4. The map ι:X→X^ sending p to the class of the constant sequence at p is an isometric embedding with dense image (def-isometry-and-metric-embedding, def-metric-interior-closure-boundary). 5. (X^,d^) is complete. Consequently ((X^,d^),ι) is a completion of (X,d) (def-metric-completion), and every metric space has a completion. The notation is kept honest. A Cauchy sequence in X need not converge in X, so no symbol lim⁡nxn appears anywhere below; the only limits taken are limits of real sequences, and each is written only after its existence has been proved. The equivalence relation is defined and verified here rather than cited, as was done for def-integers, so that the construction is self-contained and its transitivity argument is visible at the point of use. (Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences).

[F4]

Assume the ultrafilter lemma. If X is Tychonoff, e:X→[0,1]C(X,[0,1]) is its full evaluation map, and K=e[X]‾, then (K,e) is a Hausdorff compactification of X. In particular every Tychonoff space has one. This statement uses the ultrafilter lemma only for compactness of the cube; it makes no assertion about dependent choice. (Assuming the ultrafilter lemma, every Tychonoff space has a Hausdorff compactification).

[F5]

Assume the Axiom of Countable Choice. If (X,d) is a complete metric space and Y⊆X is Gδ in X, then the subspace Y is completely metrizable. (Under the Axiom of Countable Choice, every Gδ subspace of a complete metric space is completely metrizable).

[F6]

Let (X,d) be a metric space with its metric topology. Then X is Tychonoff and perfectly normal; in particular every metric space is a Tychonoff space (In a metric space every closed set is a zero set and a Gδ, and the distance function separates a point from a closed set, so every metrizable space is Tychonoff and perfectly normal).

Proof

technique · direct
1.1givenF3F1F5

The empty space has its unique compatible complete metric.

2.1step 1.1F3F1F2F6

Otherwise embed the space densely in its metric completion. The completion is a metric space, so by [F6] it is Tychonoff, which is the hypothesis [F4] requires before a compactification may be formed; compactify it, and observe that the resulting compact space is also a compactification of the original dense subspace.

3.1step 2.1F1F3F2F4

Compactification independence makes the original space Gδ there and hence in the completion.

4.1step 3.1F3F5F1

Apply the Gδ-subspace theorem to the complete metric completion.

5.1step 4.1∎

The preceding construction and implications establish the assertion.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Under the ultrafilter lemma and the Axiom of Choice, a metrizable space is Čech-complete exactly when it is completely metrizable

Statement

Assume the ultrafilter lemma and the Axiom of Choice. A metrizable space is Čech-complete if and only if it is completely metrizable.

Facts & Assumptions

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

[F1]

Assume the ultrafilter lemma and the Axiom of Choice. Every completely metrizable space is Čech-complete. (Under the ultrafilter lemma and the Axiom of Choice, every completely metrizable space is Čech-complete).

[F2]

Assume the ultrafilter lemma. Every metrizable Čech-complete space is completely metrizable. (Under the ultrafilter lemma, every metrizable Čech-complete space is completely metrizable).

Proof

technique · direct
1.1givenF1F2

The empty space lies in both classes.

2.1step 1.1F2F1

For a nonempty metrizable space combine the two preceding implications, retaining metrizability only for the direction from Čech-completeness to complete metrizability.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Every locally compact Hausdorff space is Čech-complete

Statement

Assume the Axiom of Dependent Choice. Every locally compact Hausdorff space is Čech-complete.

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; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as Gδ subspaces of Hausdorff compactifications).

[F2]

Let (X,T) be a topological space (def-topological-space) and let (X∗,T∗) be its one-point compactification, with added point ∞ (def-one-point-compactification). Then: 1. X∗ is compact (def-compact-space). 2. X is an open subspace of X∗: X∈T∗, and the subspace topology that X inherits from X∗ (def-subspace-topology-top) is T itself. 3. X is dense in X∗ (def-dense-top) if and only if X is not compact. 4. X∗ is Hausdorff (def-hausdorff-space) if and only if X is locally compact (def-locally-compact-space) and Hausdorff. In particular, a locally compact Hausdorff space is an open subspace of a compact Hausdorff space, which is the reason the construction is made. No choice principle is used: the only cover thinned below is thinned by the indexed form of lem-compactness-of-a-subspace-is-ambient, which returns its own indices. (X∗ is compact and contains X as an open subspace; X is dense in X∗ exactly when X is not compact; and X∗ is Hausdorff exactly when X is locally compact and Hausdorff).

[F3]

Let (X,T) be a topological space (def-topological-space) and let A⊆X. A is a Gδ set of X when there is a sequence (Vn)n∈N of open subsets of X with A=⋂n∈NVn, and an Fσ set of X when there is a sequence (Fn)n∈N of closed subsets of X with A=⋃n∈NFn. (Gδ and Fσ subsets of a topological space, agreeing with the real-line notion).

[F4]

Assume the Axiom of Dependent Choice. If (X,T) is locally compact and Hausdorff, then X is completely regular, and hence, being Hausdorff, Tychonoff (Under dependent choice a locally compact Hausdorff space is completely regular, hence Tychonoff).

Proof

technique · direct
1.1givenF2F1F3

The empty space is compact and is Gδ in itself.

2.1step 1.1F2F1F3F4

Čech-completeness is defined in [F1] for Tychonoff spaces only, so first record that the space qualifies: it is locally compact Hausdorff, so [F4] makes it completely regular and, being Hausdorff, Tychonoff. For a nonempty noncompact such space the one-point compactification is compact Hausdorff and contains the original space as an open subspace.

3.1step 2.1F2F1F3

An open subset is a Gδ by repeating it in a constant countable intersection, so it witnesses Čech-completeness; an already compact space is its own witness.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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→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→Y is an embedding if f is injective and the corestriction f0:X→f[X], f0(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 (Vn)n∈N of open subsets of X with A=⋂n∈NVn. 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⊆X the subspace topology on S is TS:={ U∩S:U∈T }, the family of traces on S of the open sets of X; a subset of S lying in TS 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∈T:U∩S⊆W } is a canonical member of T with U′∩S=W, for each W∈TS. (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⊆X is dense in X if A‾=X, and this is equivalent to U∩A≠∅ for every nonempty open U⊆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 (Un)n∈N of subsets of X that are open and dense in X (def-dense-top), the intersection ⋂n∈NUn 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 T1, hence X is T3 and T4. (A compact Hausdorff space is regular and normal, hence T3 and T4).

[F9]

For a topological space (X,T) the following are equivalent: (a) X is regular (def-regular-and-t3-spaces); (b) for every x∈X and every open U with x∈U there is an open V with x∈V⊆V‾⊆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∈U open gives an open V with x∈V⊆V‾⊆U).

[F10]

A‾ is closed, contains A, and is contained in every closed F⊆X with A⊆F; so it is the smallest closed superset of A, and A is closed if and only if A=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⊆X×X entire on X when for every x∈X there is y∈X with xRy. The Axiom of Dependent Choice is the statement: for every nonempty set X, every relation R entire on X, and every a∈X, there is a sequence x:N→X with x0=a and xnRxn+1 for every n∈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≠∅, where ⋂∅=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.1givenF1F2F4

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 TK be the topology of K, so K is compact Hausdorff and i:X→K is an embedding by [F2], and by [F4] there is a sequence (Gn)n∈N of members of TK with Y=⋂n∈NGn, whence Y⊆Gn for every n∈N.

1.2givenF6F7

By [F7] the assertion to be proved is that for every sequence (Un)n∈N of open dense subsets of X the set ⋂n∈NUn is dense in X, and by [F6] that says exactly that ⋂n∈NUn meets every nonempty open V⊆X; fix such a sequence (Un)n∈N and such a set V, there being nothing to prove when X has no nonempty open subset, in particular when X=∅.

2.1step 1.1step 1.2F3F5F6

By [F3] the corestriction i0:X→Y is a homeomorphism onto Y with the subspace topology inherited from K, so i[V] and every i[Un] are open in Y and i[V]≠∅; each i[Un] is moreover dense in Y, since for nonempty S open in Y the set i0−1[S] is nonempty and open in X, hence meets Un by [F6], and the image under i of a point of i0−1[S]∩Un lies in S∩i[Un]; putting W:=⋃{ O∈TK:O∩Y⊆i[V] } and Wn:=⋃{ O∈TK:O∩Y⊆i[Un] } for n∈N, the canonical tracing construction of [F5] makes these members of TK with W∩Y=i[V] and Wn∩Y=i[Un], and since Wn is defined by a formula in n rather than selected, the sequence (Wn)n∈N is obtained with no appeal to countable choice.

2.2step 1.1F8F9

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∈K and every P∈TK with y∈P there is O∈TK with y∈O⊆O‾⊆P, all closures being taken in K.

3.1step 1.1step 2.1step 2.2F6

Since i[V] is nonempty and open in Y and i[U0] is dense in Y, there is a point y0∈i[V]∩i[U0]=Y∩W∩W0, and y0∈G0 because Y⊆G0; thus y0 lies in the member W∩W0∩G0 of TK, and the closure form of regularity yields O0∈TK with y0∈O0⊆O0‾⊆W∩W0∩G0, so that O0∩Y≠∅.

3.2step 1.1step 2.1step 2.2F6

Let S:={ (n,O):n∈N, O∈TK, O∩Y≠∅ } and let R hold of ((n,O),(m,O′)) exactly when m=n+1 and O′‾⊆O∩Wm∩Gm; then R is entire on S, for given (n,O)∈S the set O∩Y is nonempty and open in Y, so the dense set i[Un+1]=Y∩Wn+1 meets it in a point y, which lies in Gn+1 because Y⊆Gn+1 and hence lies in the member O∩Wn+1∩Gn+1 of TK, and the closure form of regularity yields O′∈TK with y∈O′⊆O′‾⊆O∩Wn+1∩Gn+1, so that (n+1,O′)∈S and (n,O)R(n+1,O′).

4.1step 3.1step 3.2F11

The class S is a set, being a subset of N×TK, 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,O0) gives a sequence s:N→S with s0=(0,O0) and snRsn+1 for every n∈N; since R raises the first coordinate by exactly one, induction on n gives sn=(n,On) for members On of TK with On∩Y≠∅, and the definition of R gives On+1‾⊆On∩Wn+1∩Gn+1 for every n∈N, while O0‾⊆W∩W0∩G0 by step 3.1.

5.1step 4.1F10F12

Each On‾ is closed in K and contains the nonempty set On by [F10], hence is nonempty, and On+1‾⊆On⊆On‾ by step 4.1 and [F10], so the family { On‾:n∈N } is decreasing; a nonempty finite subfamily therefore has intersection ON‾≠∅, where N is the largest index occurring in it, and the empty subfamily has intersection K⊇O0‾≠∅, 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∈⋂n∈NOn‾.

6.1step 1.1step 2.2step 4.1step 5.1F3

For every n≥1 step 4.1 gives y∈On‾⊆Wn∩Gn, and y∈O0‾⊆W∩W0∩G0, so y∈⋂n∈NGn=Y by step 1.1, and therefore y∈Y∩Wn=i[Un] for every n∈N and y∈Y∩W=i[V] by step 2.2; as i is injective by [F3], the point x:=i0−1(y) of X lies in V and in Un for every n∈N.

7.1step 1.2step 6.1∎

Thus ⋂n∈NUn meets the arbitrary nonempty open set V, so it is dense in X by step 1.2, and X is a Baire space.

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 TK contained in some i[Un]; 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 Un 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 TK is contained in Y, and Y has empty interior in K. What steps 3.1 and 3.2 use instead is that O∩Y≠∅, which is preserved because i[Un+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 Wn are the canonical tracing sets of [F5], so passing from the relatively open i[Un] to an ambient Wn for all n at once is a definition rather than a countable choice; the Gn arrive as a sequence from [F4]; and the two individual points y0 and y are single existential instantiations.

  • Compact closures are not what the argument needs. Every On‾ 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 O0‾. What is load bearing is only that the On‾ are closed in a compact space and decrease, together with On‾⊆Gn, which is what forces the limit point into Y rather than into the remainder K∖Y.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Closed subspaces of Čech-complete spaces are Čech-complete

Statement

Every closed subspace of a Čech-complete space is Čech-complete.

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; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as Gδ subspaces of Hausdorff compactifications).

[F2]

Let (X,T) be a topological space (def-topological-space), with subspaces as in def-subspace-topology-top and compactness as in def-compact-space. Then: 1. Closed in compact is compact. If (X,T) is compact and F⊆X is closed in X, then F is a compact subset of X. 2. Finite unions. If n∈N and K0,…,Kn are compact subsets of X, then K0∪⋯∪Kn is a compact subset of X. The union of the empty list is ∅, which is a compact subset of every space. Claim 1 needs X to be compact and claim 2 does not; no hypothesis of any kind is placed on X in claim 2. No choice principle is used: claim 1 selects nothing, taking a least index where a selection would be natural, and claim 2 makes finitely many selections through lem-finite-choice, a theorem of ZF. (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[F3]

Let (X,T) be a Hausdorff topological space (def-hausdorff-space, def-topological-space), with compact subsets as in def-compact-space. Then: 1. A point and a disjoint compact set are separated. If K⊆X is compact and x∈X∖K, there are U,V∈T with x∈U,K⊆V,U∩V=∅. 2. Two disjoint compact sets are separated. If K,L⊆X are compact and K∩L=∅, there are U,V∈T with L⊆U,K⊆V,U∩V=∅. 3. Compact implies closed. Every compact subset of X is closed in X. 4. In a compact Hausdorff space the two classes coincide. If in addition (X,T) is compact, then a subset of X is compact if and only if it is closed. The proof is written choice-free, and that is not a stylistic preference. The textbook argument says "for each y∈K choose disjoint open Uy,Vy", which is a selection over an arbitrary index set and therefore an appeal to the full Axiom of Choice. What is done below instead is to take the family of all open V that admit some open U∋x disjoint from them — a family cut out by a formula, with nothing selected — extract a finite subcover from it, and only then make finitely many selections, which lem-finite-choice supplies as a theorem of ZF. (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).

Proof

technique · direct
1.1givenF1F2F3

The empty closed subspace is Gδ in its empty compactification.

2.1step 1.1F1F3F2

Otherwise, if the space is Gδ in a compactification and the subspace is closed in the space, take its closure in the compactification.

3.1step 2.1F3F2F1

Inside that compact closure, the subspace is the intersection of the inherited Gδ with an additional closed set, hence is Gδ.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the Axiom of Choice, topological sums of Čech-complete spaces are Čech-complete

Statement

Assume the Axiom of Choice. The topological sum of any family of Čech-complete spaces is Čech-complete; the empty sum is included.

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; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as Gδ subspaces of Hausdorff compactifications).

[F2]

The underlying set. Let I be a set and let Xi be a set for each i∈I. The disjoint union is ⨆i∈IXi  :=  ⋃i∈I(Xi×{i}), whose elements are the pairs (x,i) with i∈I and x∈Xi. For j∈I the j-th canonical injection is κj:Xj→⨆i∈IXi,κj(x):=(x,j). The construction is what makes the word "disjoint" honest. Each κj is injective (def-injection-surjection-bijection), since (x,j)=(x′,j) forces x=x′; the images κj[Xj]=Xj×{j} are pairwise disjoint, since the second coordinate determines j; and their union is the whole set. So no assumption that the Xi are disjoint as sets is needed, and none is made: the tag i separates the copies even when Xi=Xi′ for i≠i′. (The disjoint union (coproduct) ⨆iXi with the final topology of the canonical injections: a set is open exactly when each of its traces is).

[F3]

Let (X,T) be a topological space (def-topological-space) and let (X∗,T∗) be its one-point compactification, with added point ∞ (def-one-point-compactification). Then: 1. X∗ is compact (def-compact-space). 2. X is an open subspace of X∗: X∈T∗, and the subspace topology that X inherits from X∗ (def-subspace-topology-top) is T itself. 3. X is dense in X∗ (def-dense-top) if and only if X is not compact. 4. X∗ is Hausdorff (def-hausdorff-space) if and only if X is locally compact (def-locally-compact-space) and Hausdorff. In particular, a locally compact Hausdorff space is an open subspace of a compact Hausdorff space, which is the reason the construction is made. No choice principle is used: the only cover thinned below is thinned by the indexed form of lem-compactness-of-a-subspace-is-ambient, which returns its own indices. (X∗ is compact and contains X as an open subspace; X is dense in X∗ exactly when X is not compact; and X∗ is Hausdorff exactly when X is locally compact and Hausdorff).

[F4]

The Axiom of Choice (AC) is the following statement. The statement is: every family of nonempty sets has a choice function; that is, for every set F all of whose members are nonempty there is a function g with domain F satisfying g(S)∈S for every S∈F. (The Axiom of Choice).

Proof

technique · direct
1.1givenF3F1F2F4

Choose compactification witnesses Ki for the summands and form their topological sum K:=⨆iKi, which is Hausdorff and contains ⨆iXi densely. Two cases arise, because [F3] makes K dense in K∗ exactly when K is not compact. If K is compact — in particular whenever the family is finite, as for a single one-point summand — then K is itself a Hausdorff compactification of the sum and no point is adjoined. Otherwise K is noncompact, and its one-point compactification K∗ is a Hausdorff compactification of the sum.

2.1step 1.1F3F1

Express the original sum by one countable family of open layers, using the same layer number in every clopen summand.

3.1step 2.1F3

Verify the empty sum separately.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Under the Axiom of Choice, countable products of Čech-complete spaces are Čech-complete

Statement

Assume the Axiom of Choice, which supplies both the countable selections and the Tychonoff compactness used below. A countable product of Čech-complete spaces is Čech-complete, including the empty product.

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; thm-cech-completeness-is-independent-of-compactification proves the equivalent every-compactification form. (Čech-complete spaces as Gδ subspaces of Hausdorff compactifications).

[F2]

Assume the Axiom of Choice (def-axiom-of-choice). Let I be a set and let (Xi,Ti)i∈I be a family of compact topological spaces (def-compact-space, def-topological-space). Then the product P  :=  ∏i∈IXi with the product topology (def-product-topology) is compact. The Axiom of Choice is spent twice, and both uses are flagged below. Once inside thm-alexander-subbase-lemma, through Zorn's lemma (thm-zorn), and once directly at step 2.1, to produce a point of a product of nonempty sets. (Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice).

[F3]

The Axiom of Countable Choice, written ACω, is the following statement. The statement is: for every family (Xn)n∈N of nonempty sets indexed by N there is a function f with domain N such that f(n)∈Xn for every n∈N. Equivalently, every at most countable family of nonempty sets has a choice function. (The Axiom of Countable Choice (ACω)).

[F4]

N×N≈N (def-equinumerous): the plane of pairs of naturals is countably infinite (def-countable). The bijection is exhibited, not merely asserted to exist. Define 2m by recursion on m (thm-recursion) by 20=1 and 2σ(m)=2m+2m, and set J(m,n)=2m⋅σ(n+n),that isJ(m,n)=2m(2n+1). Then J is a bijection from N×N onto N∖{0}, and σ is a bijection from N onto N∖{0}, so σ−1∘J is a bijection N×N→N. What makes J bijective is the decomposition of a nonzero natural into a power of two times an odd number, existence and uniqueness both. (N×N≈N).

[F5]

The product set. Let I be a set and let Xi be a set for each i∈I. The product is ∏i∈IXi  :=  { x:x is a function with domain I and x(i)∈Xi for every i∈I }, and we write xi:=x(i), the i-th coordinate of x. Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For j∈I the j-th projection is πj:∏i∈IXi→Xj,πj(x):=xj.. The product topology TΠ on ∏iXi is the initial topology of the projections: the topology generated by the subbasis {πi−1[U]:i∈I, U∈Ti}. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes ∏i∈IUi with every Ui open in Xi and Ui=Xi for all but finitely many i. (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

Proof

technique · direct
1.1givenF1

Choose compactification witnesses and Gδ presentations for the factors.

2.1step 1.1F2F5F4F3

Their compact product is compact by Tychonoff, and the product of the original spaces is the countable intersection over pairs of a coordinate and a layer of open cylinder sets.

3.1step 2.1F2F5F4

Pair the two natural indices and include the empty product.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

5 · Examples, counterexamples and false statements

None yet.

Sources