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.
Every open subspace of a completely metrizable space is completely metrizable
Statement
If is completely metrizable and is open, then is completely metrizable in its subspace topology.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
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).
Let be a metric space (def-metric-space), let be nonempty and let . Then with the distance to a nonempty set (def-metric-bounded-diameter). Thus the real-valued function changes by at most between and : it is -Lipschitz. (, so the distance to a fixed nonempty set is -Lipschitz).
Proof
If , its unique metric is compatible and complete. Otherwise choose a complete metric on compatible with its given topology, as allowed by [F1]. Since is open, it is also -open.
If , the restricted metric is compatible and complete. Hence assume is nonempty and proper, and put . Then is nonempty and -closed. For , let . Openness of gives , and [F2] gives .
Define on . This is a metric: it is nonnegative and symmetric, vanishes only when because is a metric, and satisfies the triangle inequality by adding those for and absolute value. Also .
The metrics and induce the same topology. Indeed, fix and . If , then by [F2], so . Thus implies . Conversely implies by step 3.1.
Let be -Cauchy. Then is -Cauchy and the real sequence is Cauchy by step 3.1. Completeness of gives a limit , and every Cauchy real sequence is bounded, so for some finite and all . Hence ; [F2] and imply . If , its distance to would be zero, so .
Since and , the reciprocal estimate of step 4.1 gives . Therefore , 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 is completely metrizable.
Depends on
Used by
Dependency tree · two levels
34 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
- 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)