Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-05 (gpt-5.6-sol-codex-subscription)
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.

On an ordinal with its order topology the sets [0,β] and (α,β] form a basis of clopen sets, the isolated points are exactly the non-limit ordinals, and the space is Hausdorff

Statement

Let γ be an ordinal (Ordinal (von Neumann)), regarded as the set of ordinals below it, linearly ordered by membership (Trichotomy and well-ordering of the ordinals), and give it the order topology (The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua). For α,β∈γ write

[0,β]:={ ξ∈γ:ξ≤β },(α,β]:={ ξ∈γ:α<ξ≤β }.

Then:

  1. Every set of either form is clopen (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), and Bγ  :=  { [0,β]:β∈γ }  ∪  { (α,β]:α,β∈γ } is a basis for the order topology of γ (Basis and subbasis for a topology, and the topology generated by a family of sets).
  2. The isolated points of γ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space) are exactly the ordinals ξ∈γ that are 0 or a successor; a limit ordinal ξ∈γ (Successor and limit ordinals) is not isolated.
  3. γ with its order topology is Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

Regularity is not claimed here, and nothing below asserts any separation property beyond claim 3; the finer separation axioms are not available at this point in the reading order.

Facts & Assumptions

Given: An ordinal γ with the order topology of the membership order on it.

[L1]

γ is the set of the ordinals below it; membership is a strict linear order on it, α≤β abbreviates "α∈β or α=β", and α⊆β holds exactly when α≤β (Ordinal (von Neumann), Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals, Partial order and partially ordered set).

[L3]

A family of open sets is a basis for a topology exactly when every open U and every x∈U admit a member B of the family with x∈B⊆U (Basis and subbasis for a topology, and the topology generated by a family of sets).

[L4]

Arbitrary unions and finite intersections of open sets are open, and a set is closed exactly when its complement is open (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L5]

β+=β∪{β} is an ordinal, and for ordinals β<α holds exactly when β+≤α: from β∈α one gets β⊆α and {β}⊆α, hence β+⊆α, and conversely β∈β+⊆α. Every ordinal is 0, a successor or a limit ordinal (Basic closure properties of ordinals, Successor and limit ordinals, Ordinal (von Neumann)).

[L6]

A point x of a space X is isolated exactly when {x} is open, since a neighbourhood N of x with N∩X={x} contains an open U with x∈U⊆{x}, and conversely (Interior, closure, boundary, exterior, derived set and isolated point in a topological space, Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).

Proof

technique · direct
1.1

For β∈γ the set [0,β] is open: if β+∈γ then ξ≤β is equivalent to ξ<β+ by [L5], so [0,β]=γ<β+, an open ray; and if β+∉γ then β+⊆γ, since every ordinal below β+ is ≤β and so lies in γ, whence β+=γ by [L1] and [0,β]=γ, which is open.

L1L2L4L5
1.2

For ξ≠η in γ the trichotomy of [L1] gives ξ<η after renaming. By [L5] the inequality ξ<η gives ξ+≤η, and since η∈γ, [L1] puts ξ+ in γ as well; so γ<ξ+ and γ>ξ are open rays, and they contain ξ and η respectively, since ξ<ξ+ and ξ<η. They are disjoint: a common point ζ would satisfy ζ<ξ+, hence ζ≤ξ by [L5] and trichotomy, and ξ<ζ at once, which [L1] forbids. So claim 3 holds by [L7].

L1L2L5L7
2.1

For α,β∈γ the set (α,β]=γ>α∩[0,β] is open by [L4], being an intersection of two open sets.

L2L4step 1.1
2.2

Every set [0,β] is closed, its complement being the open ray γ>β.

L2L4step 1.1
3.1

Every set (α,β] is closed: its complement in γ is [0,α]∪γ>β, a union of an open set by step 1.1 and an open ray, hence open by [L4]. So every member of Bγ is clopen.

L2L4step 1.1step 2.1step 2.2
3.2

Claim 2, the isolated points. The point 0 is isolated when 0∈γ, since {0}=[0,0] is open by step 1.1; and a successor ξ=η+∈γ is isolated, since η<ξ puts η in γ and {ξ}=(η,ξ] is open by step 2.1.

L5L6step 1.1step 2.1
4.1

Bγ is a basis. Let U be open and ξ∈U; by [L2] and [L3] there is a set B among γ, the open rays and the open intervals with ξ∈B⊆U. If B=γ or B=γ<b, then [0,ξ] contains ξ and lies inside B, since η≤ξ gives η<b in the second case. If B=γ>a or B=(a,b), then a<ξ and (a,ξ] contains ξ and lies inside B. In each case a member of Bγ sits between ξ and U, and its members are open by step 1.1 and step 2.1, so [L3] applies and claim 1 is proved.

L2L3step 1.1step 2.1step 3.1
5.1

Conversely let ξ∈γ be a limit ordinal. Were {ξ} open, step 4.1 would supply B∈Bγ with ξ∈B⊆{ξ}, so B={ξ}. If B=[0,β] then β=ξ and 0∈B, forcing ξ=0, which no limit ordinal is. If B=(α,ξ] with α<ξ then α+≤ξ by [L5], and α+≠ξ because ξ is not a successor, so α<α+<ξ puts α+ in B alongside ξ. Both cases are impossible, so {ξ} is not open and ξ is not isolated by [L6]; with step 3.2 this is claim 2.

L5L6step 3.2step 4.1∎

Remarks

Why the half-open sets and not the open intervals. In an ordinal every point other than a limit is isolated, and the sets (α,β] are the convenient basic sets that always stay clopen: an open interval (α,β) need not be closed, while (α,β] always is, because its complement is again a union of sets of the two admissible forms. That every basic set is clopen is what makes an ordinal space totally disconnected in the naive sense and is used repeatedly in Every successor ordinal is compact in its order topology and every limit ordinal is not; and, assuming countable choice, ω1 is countably compact and sequentially compact while ω1+1 is compact.

The topology defined here is the general order topology and not a second notion. It is The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua applied to the linearly ordered set γ, and claim 1 says only that the general basis of rays and intervals may be replaced by the more convenient Bγ. A published item elsewhere in the library states the same topology on an ordinal directly, as def-order-topology-on-an-ordinal; it is named here in plain text because its page comes later in the reading order, and the agreement between the two descriptions is exactly claim 1.

The greatest-element case is not an edge case to be waved through. When γ is a successor δ+ its greatest element is δ and [0,δ]=γ; step 1.1 treats that case explicitly, and it is the case that makes a successor ordinal compact (Every successor ordinal is compact in its order topology and every limit ordinal is not; and, assuming countable choice, ω1 is countably compact and sequentially compact while ω1+1 is compact).

Depends on

Used by

Dependency tree · two levels

36 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