Alphabeta Math
LemmaStatement: 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, 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.

Depends on

Used by

Dependency tree · two levels

46 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