Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)
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.

A linear continuum is connected in its order topology, and so is every order-convex subset of it

Statement

Let (L,≤) be a linear continuum: a linearly ordered set with at least two elements that is order-dense and has the least upper bound property (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). Give L its order topology. Then:

  1. L is connected (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).
  2. Every order-convex C⊆L, with the subspace topology, is connected. In particular every interval [a,b], (a,b), [a,b), (a,b] and every ray of L is connected.

Claim 2 covers the degenerate cases: ∅ and every singleton are order-convex and connected.

Facts & Assumptions

Given: A linear continuum (L,≤) with its order topology, and an order-convex C⊆L.

[A1]

The order is linear, so any two elements are comparable and exactly one of x<y, x=y, y<x holds; ≤ is transitive and antisymmetric (Partial order and partially ordered set).

[A2]

Order-density: for x<y in L there is z with x<z<y. Least upper bound property: a nonempty subset with an upper bound has a least upper bound sup⁡, which is an upper bound and is ≤ every upper bound (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, Upper bound, least upper bound, and strict upper bound).

[A3]

{L}∪{L<q}∪{L>p}∪{(p,q)} is a basis for the order topology, so every open set containing a point contains a member of that family containing it (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, Basis and subbasis for a topology, and the topology generated by a family of sets).

[A4]

A separation of a space is a pair of open, nonempty, disjoint sets whose union is the space; a space is connected when none exists; ∅ and every one-point space are connected (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

technique · contradiction
1.1

Suppose, for contradiction, that (U,V) is a separation of L: both open and nonempty, disjoint, with U∪V=L.

assume-contraA4
2.1

Fix a∈U and b∈V. They are distinct, U and V being disjoint, so by [A1] one is below the other; relabelling U and V if necessary, which is legitimate because the hypothesis of step 1.1 is symmetric in them, assume a<b.

step 1.1A1
3.1

Put S:={ t∈U:a≤t≤b }. It is nonempty, containing a, and b is an upper bound of it, so c:=sup⁡S exists by [A2] and satisfies a≤c≤b, since a∈S and b is an upper bound.

step 2.1A2
4.1

Suppose c∈V. Then c≠a, since a∈U and the two sets are disjoint, so a<c by [A1] and a≤c. By [A3] there is a basic open W with c∈W⊆V; W is neither L nor a set L<q, since either would contain a, giving a∈V. So W is L>p or (p,q) with p<c, and in both cases (p,c]⊆W⊆V.

step 1.1step 3.1A1A3
4.2

Suppose instead c∈U. Then c≠b, so c<b by [A1] and c≤b. By [A3] there is a basic open W with c∈W⊆U; W is neither L nor a set L>p, since either would contain b, giving b∈U. So W is L<q or (p,q) with c<q, and in both cases [c,q)⊆W⊆U; moreover q≤b, since b∉U and c<b would otherwise put b in [c,q).

step 1.1step 3.1A1A3
5.1

In the case of step 4.1, p<c=sup⁡S, so p is not an upper bound of S by [A2] and there is s∈S with p<s≤c; then s∈(p,c]⊆V and s∈U, contradicting U∩V=∅.

step 1.1step 3.1step 4.1A2
5.2

In the case of step 4.2, order-density gives z with c<z<q by [A2]; then z∈[c,q)⊆U, and a≤c<z<q≤b, so z∈S while z>c=sup⁡S, contradicting that sup⁡S is an upper bound of S.

step 3.1step 4.2A2
6.1

By step 1.1 the point c lies in U∪V=L, so one of the two cases applies, and each is contradictory by steps 5.1 and 5.2. Hence no separation of L exists and L is connected; this is claim 1.

step 1.1step 5.1step 5.2A4
7.1

For claim 2 let C⊆L be order-convex. If C has at most one element it is connected by [A4]. Otherwise C carries the order topology of its restricted order by [A5], and C is itself a linear continuum: it has at least two elements; it is order-dense, because for x<y in C the element z with x<z<y given by [A2] lies in C by order-convexity; and it has the least upper bound property, because a nonempty S⊆C with an upper bound u∈C has sup⁡S in L by [A2], and s≤sup⁡S≤u for any s∈S puts sup⁡S in C by order-convexity, where it is again the least upper bound. So claim 1 applies to C.

step 6.1A2A4A5discharge-contradiction∎

Remarks

  • Both hypotheses are spent, each exactly once. The least upper bound property produces c at step 3.1, and order-density produces the point z at step 5.2. Neither may be dropped. An ordered set with a jump, a pair x<y with (x,y)=∅, is separated by the two open sets L<y and L>x, which is what density forbids; and the rationals, which are order-dense but lack the least upper bound property, are separated by {q:q2<2 or q<0} and its complement, both open.

  • Why the argument is asymmetric between the two cases. Case 4.1 needs only that c is a least upper bound; case 4.2 needs a point strictly above c inside U, and only density supplies one. That asymmetry is intrinsic: a supremum can be approached from below in any ordered set, and stepping strictly above it while staying inside a small open set is what requires there to be no gaps.

  • Claim 2 is proved by re-reading C as a continuum, not by a second argument. The two facts that make this legal are that an order-convex subset carries its own order topology as a subspace, and that order-density and the least upper bound property are inherited by order-convex subsets. Both are established at step 7.1 rather than assumed.

Depends on

Used by

Dependency tree · two levels

28 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