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.
Nice refinements exist and are regular but not Lindelof
Statement
Every ordered fundamental space has a nice refinement satisfying for every . The refinement is separable, locally compact, locally countable, zero-dimensional, regular, and Hausdorff, but it is not Lindelöf. Here locally countable means that every point has a countable neighbourhood.
Facts & Assumptions
Given: An ordered fundamental space and ZFC.
Ordered fundamental spaces and nice refinements gives the rings, intermediate topologies, model chain, metrics, nice-refinement clauses, the families , and .
A compact topological space is one whose every open cover has a finite subcover, and a compact subset carries the intrinsic subspace topology (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).
A compact metric space is totally bounded: at every positive radius it has a finite net (A compact metric space is complete and totally bounded, and neither implication uses any choice principle).
A space is locally compact when every point has a compact neighbourhood (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space).
A space is Lindelöf when every open cover has an at most countable subcover (Countably compact, Lindel"of, sequentially compact, limit point compact and -compact spaces, and relatively compact subsets).
A clopen base gives the point--closed-set separation required for regularity (Regular spaces and spaces, with the source disagreement over whether regularity includes stated explicitly).
Countable elementary submodels and their collapses supplies a countable elementary hull containing any prescribed countable parameter set.
Transfinite recursion constructs the model chain and the later stage-by-stage refinement from their functional successor and limit clauses.
The Axiom of Choice supplies the simultaneous recursive choices of hulls, metrics, finite nets, ring points, and compact clopen enlargements.
Proof
Construct the required continuous chain explicitly. Start with an F7 hull containing the ordered fundamental space and its base assignment. At a successor, apply F7 to the countable set and the fixed parameters; at a countable limit take the union of the earlier increasing elementary chain, which is countable and elementary by the Tarski--Vaught test. F8 performs this recursion, and F9 makes the simultaneous hull choices. Now choose the compatible metrics allowed by F1 and F9. For put . Inductively suppose the and have been constructed for every , and that the resulting topology below is locally compact and zero-dimensional.
Fix . The countable model contains only countably many sets satisfying and ; list them as , repeating every such infinitely often. This collection is nonempty because it contains , and that particular makes the later star implication vacuous.
Recursively suppose is fixed for and put . This is a finite union of compact sets, hence compact. Every lies in : the first ring intersections lie in their , while all remaining points lie in the nested .
The family has a finite Hausdorff -net chosen from itself. Indeed, by [F3] choose a finite -net of the compact metric set , where . Partition the remaining tail into the outer ring and the deeper tail . Record for each which finitely many -cells meet , whether meets , and whether it meets . There are finitely many records. Two compacta with the same record are within Hausdorff distance at most : match their points in through a common recorded cell; points in are within its internal diameter ; and points in are within by the triangle inequality, since every such point has distance at most from . The two tail-incidence bits ensure that each required matching part is nonempty. Choosing one member for each realized record gives ; if , take .
Let be the union of over . It is a compact subset of the relatively clopen nonempty -th ring. Local compactness and the clopen base below cover by finitely many compact clopen sets lying in that ring; their union is compact clopen. If this union is empty, choose a ring point and one compact clopen neighbourhood of it in the ring. Call the resulting nonempty compact clopen set ; it contains .
For , membership in already puts its intersections with rings inside . For , the stage- definition includes in , so absorbs the -th ring intersection of . Hence .
Put . Its maximum is and its part below is open. It is compact in the intermediate topology: an intermediate-open cover has a member containing , hence contains some and all for ; only finitely many earlier compact remain. It is therefore intermediate-closed, and [F1] makes the a clopen local base in the final refinement. The same argument for a final-open cover, now using a contained , proves that is compact in the final topology.
Whenever , steps 4.1 and 6.1 give . Every relevant occurs infinitely often, so holds.
Steps 2.1--7.1 together with step 6.2 perform the successor construction at every countable , while limit stages take the accumulated earlier data. Transfinite induction therefore produces a nice refinement satisfying every .
Every is compact by step 6.2, so [F4] gives local compactness. It lies in , a countable ordinal, so it is a countable neighbourhood and the space is locally countable. The base is clopen and Hausdorff by [F1], hence zero-dimensional and regular by [F6].
The set remains dense. Inductively, every nonempty relatively open meets the already dense , so every basic tail meets ; for the singleton itself lies in . Thus the refinement is separable.
Every initial segment is open: if , then each basic neighbourhood is contained in . Consequently is an open cover of . A countable subfamily has countable supremum and its union is contained in , so it misses . By [F5] the refined space is not Lindelöf.
Combining steps 7.1 and 8.1--9.3 gives all asserted properties. The empty cases were handled in steps 2.1 and 4.1, has , the finite ordinals use singleton bases, and F9 records every nonempty simultaneous choice.
Depends on
- Ordered fundamental spaces and nice refinements
- Regular spaces and $T_3$ spaces, with the source disagreement over whether regularity includes $T_1$ stated explicitly
- Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
- Countably compact, Lindel\"of, sequentially compact, limit point compact and $\sigma$-compact spaces, and relatively compact subsets
- Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space
- A compact metric space is complete and totally bounded, and neither implication uses any choice principle
- Countable elementary submodels and their collapses
- Transfinite recursion
- The Axiom of Choice
Used by
Dependency tree · two levels
53 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
- Hart–Kunen, Ultra Strong S-Spaces, Lemmas 4.5, 4.8 and 4.12, printed pp. 96–100 (standard reference, not scraped)