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.
Stone's theorem, under choice: every metric space is paracompact
Statement
Assume the Axiom of Choice. Every metric space is paracompact.
Facts & Assumptions
Given: The Axiom of Choice, a metric space , and an arbitrary open cover of its metric topology.
Under choice, every metric open cover has a point-finite open refinement, and Ornstein's second construction turns that point-finite cover into a locally finite open refinement (Under choice, every open cover of a metric space has a point-finite open refinement, Under choice, Ornstein's second construction turns a point-finite metric open cover into a locally finite open refinement).
Paracompactness means that every open cover has such a refinement (Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word).
Proof
Apply [L1] to the arbitrary cover .
The resulting locally finite open refinement is exactly the condition in [F1], so is paracompact.
Remarks
The theorem is proved here with the Axiom of Choice as a sufficient hypothesis. No assertion is made that this is its exact set-theoretic strength.
Depends on
- Under choice, every open cover of a metric space has a point-finite open refinement
- Under choice, Ornstein's second construction turns a point-finite metric open cover into a locally finite open refinement
- Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word
- Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric
- The Axiom of Choice
Used by
- Under choice and dependent choice, metric open covers admit locally finite subordinate partitions of unity Corollary
- Under choice, the Niemytzki plane is Tychonoff and locally metrizable but not normal, paracompact, or metrizable Example
- Under choice, every metric space has a σ-locally-finite basis Lemma
- Choice and convention ledger for paracompactness, Stone's theorem, and partitions of unity Remark
- Under choice, a space is metrizable if and only if it is paracompact, Hausdorff, and locally metrizable Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 57 results over 13 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
- D. Ornstein, A New Proof of the Paracompactness of Metric Spaces, Proc. Amer. Math. Soc. 21 (1969), 341–342 (standard reference, not scraped)
- C. Good, I. J. Tree and W. S. Watson, On Stone's theorem and the axiom of choice (standard reference, not scraped)
- Topology 262 notes (California State University, Northridge) (standard reference, not scraped)