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.
Assuming choice, two paracompact lower-limit lines can have a nonparacompact product
Statement refuted
Assuming the Axiom of Choice, a product of paracompact spaces is paracompact.
Facts & Assumptions
Given: The lower-limit line under the Axiom of Choice.
Choice implies countable choice (The Axiom of Choice, The Axiom of Countable Choice ()).
If in , then and are disjoint open neighbourhoods, so is Hausdorff (The lower-limit topology on , with the half-open intervals as a basis, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).
The lower-limit line is regular and Lindelöf; under countable choice every regular Lindelöf space is paracompact (The lower-limit line has a clopen basis, is regular, and is Lindelöf under countable choice, Under countable choice, every regular Lindelöf space is paracompact).
Under choice, is not normal (Assuming choice, normality is not productive: the normal lower-limit line has a nonnormal square).
The product of Hausdorff spaces is Hausdorff (Arbitrary products preserve , , and Hausdorffness).
A paracompact Hausdorff space is normal (Every paracompact Hausdorff space is normal).
Counterexample
By [A1] and [L1], both factors are paracompact.
If were paracompact, [F1] and [L3] would make it Hausdorff, and [L4] would then make it normal, contradicting [L2].
Thus two paracompact spaces have a nonparacompact product, refuting the displayed assertion.
Depends on
- The lower-limit line has a clopen basis, is regular, and is Lindelöf under countable choice
- Under countable choice, every regular Lindelöf space is paracompact
- Assuming choice, normality is not productive: the normal lower-limit line has a nonnormal square
- Arbitrary products preserve $T_0$, $T_1$, and Hausdorffness
- Every paracompact Hausdorff space is normal
- The lower-limit topology on $\mathbb{R}$, with the half-open intervals $[a,b)$ as a basis
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
- The Axiom of Choice
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
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: 142 results over 22 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
- G. Gruenhage, General Topology Course Notes, Sorgenfrey plane and Jones's lemma (standard reference, not scraped)
- R. Gardner, Notes on Munkres Section 41: Paracompactness (East Tennessee State University) (standard reference, not scraped)
- Sorgenfrey topology (Encyclopedia of Mathematics) (standard reference, not scraped)