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 ordinal with its order topology has a basis of clopen sets, and is , Hausdorff and regular
Statement
Let be an ordinal (Ordinal (von Neumann)) with its order topology (The order topology on an ordinal, with the half-open intervals and the initial segments as a basis), whose basis is . Then:
- Every member of is clopen in (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), so has a basis of clopen sets.
- is ( (Kolmogorov) and (Frechet) spaces).
- is Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).
- is regular (Regular spaces and spaces, with the source disagreement over whether regularity includes stated explicitly), and therefore .
Facts & Assumptions
Given: An ordinal with its order topology, ordinals , and the basis consisting of the sets for and for in .
and , and is a basis for the order topology (The order topology on an ordinal, with the half-open intervals and the initial segments as a basis, Basis and subbasis for a topology, and the topology generated by a family of sets).
For ordinals exactly one of , , holds, and is transitive; every element of an ordinal is an ordinal (Trichotomy and well-ordering of the ordinals, Basic closure properties of ordinals, Ordinal (von Neumann)).
A set is open exactly when each of its points lies in a basic set inside it; a set is closed exactly when its complement is open; a union of open sets is open (Basis and subbasis for a topology, and the topology generated by a family of sets, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).
A space is exactly when every singleton is closed (A space is if and only if every singleton is closed, if and only if every finite subset is closed, if and only if its topology contains the cofinite topology, clause (b), (Kolmogorov) and (Frechet) spaces).
The basic sets containing a point form a neighbourhood base at that point, consisting of open sets (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).
A space is regular exactly when every point has a neighbourhood base of closed neighbourhoods (A space is regular if and only if every point has a neighbourhood base of closed neighbourhoods, if and only if open gives an open with , clause (c), Regular spaces and spaces, with the source disagreement over whether regularity includes stated explicitly).
A closed neighbourhood of a point is a neighbourhood of it that is closed, and for such a (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).
Proof
The set is open for every : if with then is a basic set with , by [A1] and transitivity in [L1].
The set is open for every : if then is a basic set with , again by [A1] and transitivity.
Let in and assume without loss of generality, by [L1]. Then and are basic open sets with , and by [A1] and trichotomy; so is Hausdorff, which is claim 3.
by trichotomy, so is closed by step 1.1 and [L2]; and is open, being basic.
by trichotomy, where is basic open and is open by step 1.1, so is closed by [L2]; and it is open, being basic.
by trichotomy, which is open by steps 1.1 and 1.2 and [L2], so is closed.
Steps 2.1 and 2.2 exhaust , so every basic set is clopen, which is claim 1.
Step 2.3 makes every singleton closed, so is by [L3], which is claim 2.
Let and let be a neighbourhood of ; by [L4] there is a basic with , and is closed by step 3.1 and open, hence a closed neighbourhood of inside .
By step 4.1 every point of has a neighbourhood base of closed neighbourhoods, so is regular by [L5]; with step 3.2 it is , which is claim 4.
Remarks
-
The clopen basis is the whole content. A space with a basis of clopen sets is regular for the reason given in step 4.1, and the ordinals have such a basis because a half-open interval has an immediate left endpoint outside it, namely , and everything above is separated from it by a further half-open interval. No case distinction between successors and limits is needed anywhere in the proof.
-
Regularity is claimed and normality is not. Nothing above asserts that an ordinal with its order topology is normal, and nothing on this page proves it. The companion page's deleted plank is a subspace of a product of two ordinal spaces and is not normal, so no normality statement about ordinal spaces may be read off from this lemma in either direction.
-
No choice principle is used, every ingredient being a theorem of ZF (Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals).
Depends on
- The order topology on an ordinal, with the half-open intervals $(\alpha, \beta]$ and the initial segments $[0, \beta]$ as a basis
- $T_0$ (Kolmogorov) and $T_1$ (Frechet) spaces
- A space is $T_1$ if and only if every singleton is closed, if and only if every finite subset is closed, if and only if its topology contains the cofinite topology
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
- Regular spaces and $T_3$ spaces, with the source disagreement over whether regularity includes $T_1$ stated explicitly
- A space is regular if and only if every point has a neighbourhood base of closed neighbourhoods, if and only if $x \in U$ open gives an open $V$ with $x \in V \subseteq \overline{V} \subseteq U$
- Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
- Interior, closure, boundary, exterior, derived set and isolated point in a topological space
- Basic closure properties of ordinals
- Trichotomy and well-ordering of the ordinals
- Ordinal (von Neumann)
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Basis and subbasis for a topology, and the topology generated by a family of sets
Used by
- Assuming choice, paracompactness is not open-hereditary: ω₁ inside ω₁+1 Counterexample
- Refuted, assuming countable choice: every Hausdorff space built from ordinal spaces is normal. The deleted Tychonoff plank ((ω₁ + 1) × (ω + 1)) ∖ {(ω₁, ω)} is Hausdorff and not normal Counterexample
- Assuming choice, ω₁ is countably compact, noncompact, and not paracompact Example
- ω + 1 as a convergent sequence together with its limit, and, assuming countable choice, [0, ω₁), in which every sequence lies inside an at most countable initial segment Example
- Assuming choice, refuted: paracompactness is hereditary False statement
- Assuming countable choice, the deleted Tychonoff plank is a regular nonnormal open subspace of a compact Hausdorff normal space Lemma
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 85 results over 19 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
- Order topology (Wikipedia) (standard reference, not scraped)
- Ordinal number (Wikipedia) (standard reference, not scraped)
- J. Munkres, Topology, 2nd ed., §14 (standard reference, not scraped)
- R. Gardner, Introduction to Topology, notes on Munkres Section 17: Closed Sets and Limit Points (East Tennessee State University) (standard reference, not scraped)
- R. Gardner, Introduction to Topology, notes on Munkres Section 32: Normal Spaces (East Tennessee State University) (standard reference, not scraped)