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.
Open and closed subspaces of a completely metrizable space are completely metrizable, and under Dependent Choice so is every 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 subspace.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
If is completely metrizable and is open, then is completely metrizable in its subspace topology. (Every open subspace of a completely metrizable space is completely metrizable).
Assume Dependent Choice. For a subspace of a complete metric space , is completely metrizable if and only if is a subset of . (Alexandrov's theorem, under Dependent Choice: a subspace of a complete metric space is completely metrizable exactly when it is ).
Let be a metric space (def-metric-space) and let carry the subspace metric (def-isometry-and-metric-embedding). Then: 1. If is complete (def-complete-metric-space), then is closed in (def-metric-topology). No hypothesis on is needed. 2. If is complete and is closed in , then is complete. Consequently, for a complete a subset is complete if and only if it is closed. (A subspace of a complete metric space is complete iff it is closed, and a complete subspace of any metric space is closed).
Let be a metric space (def-metric-space) and let be its metric topology (def-metric-topology). Call completely metrizable if some metric on is topologically equivalent to , that is (def-equivalent-metrics), and makes complete (def-complete-metric-space). Then: 1. Homeomorphism invariance. Let be a metric space and let be a bijection (def-injection-surjection-bijection) such that and are continuous (def-metric-continuity). If is completely metrizable then so is . 2. Closed subspaces. If is completely metrizable and is closed in , then is completely metrizable, being the subspace metric (def-isometry-and-metric-embedding). 3. The property is strictly weaker than completeness. Let (def-interval) carry (lem-real-line-is-a-metric-space). Then is not complete, while is a complete metric on with . So is completely metrizable although no completeness assumption holds for 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 has it without being complete).
Proof
Use the open-subspace lemma directly.
Choose a compatible complete metric for the ambient space; closed subsets are complete for its restriction, while arbitrary subsets fall under Alexandrov's theorem.
Include the empty subspace.
The preceding construction and implications establish the assertion.
Depends on
- Every open subspace of a completely metrizable space is completely metrizable
- Alexandrov's theorem, under Dependent Choice: a subspace of a complete metric space is completely metrizable exactly when it is $G_\delta$
- A subspace of a complete metric space is complete iff it is closed, and a complete subspace of any metric space is closed
- Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and $(0,\infty)$ has it without being complete
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 83 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- David Marker, Descriptive Set Theory, §§1–2 (standard reference, not scraped)
- Michael Kunzinger, General Topology, §§11.3–11.4 (standard reference, not scraped)
- MFF General Topology course summary, §4.3 (standard reference, not scraped)
- Jesse Peterson, Real Analysis, §§3.6–3.7 (standard reference, not scraped)