Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Under 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.

Depends on

Used by

Dependency tree · two levels

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

Sources