Alphabeta MathHow 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 paracompact Hausdorff space is normal
Statement
Every paracompact Hausdorff topological space is normal. No choice principle is used.
Facts & Assumptions
Given: A paracompact Hausdorff space and disjoint closed subsets .
The space is regular (Every paracompact Hausdorff space is regular).
A locally finite family commutes with closure under union (Locally finite families remain locally finite after taking closures, closure commutes with their union, and a locally finite union of closed sets is closed).
Paracompactness supplies a locally finite open refining cover (Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word).
Normality is separation of disjoint closed sets by disjoint open sets (Normal spaces and spaces, with the source disagreement over whether normality includes stated explicitly).
Proof
For each , regularity supplies an open containing with ; therefore the family of all such , together with , is an open cover of .
Take a locally finite open cover refining , and set .
The open set contains , because a member of containing a point of cannot lie inside .
Every member used in lies in one of the eligible and so has ; hence is disjoint from by [L2].
The open sets and contain and respectively and are disjoint, so [F2] proves normality.
Depends on
- Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word
- Every paracompact Hausdorff space is regular
- Locally finite families remain locally finite after taking closures, closure commutes with their union, and a locally finite union of closed sets is closed
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
- Normal spaces and $T_4$ spaces, with the source disagreement over whether normality includes $T_1$ stated explicitly
Used by
- Assuming choice, two paracompact lower-limit lines can have a nonparacompact product Counterexample
- Under choice, the Niemytzki plane is Tychonoff and locally metrizable but not normal, paracompact, or metrizable Example
- Assuming choice, refuted: paracompactness is productive False statement
- Choice and convention ledger for paracompactness, Stone's theorem, and partitions of unity Remark
- Under choice and dependent choice, every open cover of a paracompact Hausdorff space admits a locally finite subordinate partition of unity Theorem
Dependency tree · two levels
17 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
- Dartmouth Point-Set Topology, Lecture 25 (standard reference, not scraped)
- R. Gardner, Notes on Munkres Section 41: Paracompactness (East Tennessee State University) (standard reference, not scraped)