Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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,)(L, \le) 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 LL its order topology. Then:

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

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

Facts & Assumptions

Given: A linear continuum (L,)(L, \le) with its order topology, and an order-convex CLC \subseteq L.

[A1]

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

[A2]

Order-density: for x<yx < y in LL there is zz with x<z<yx < z < y. Least upper bound property: a nonempty subset with an upper bound has a least upper bound sup\sup, which is an upper bound and is \le 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)}\{L\} \cup \{L_{<q}\} \cup \{L_{>p}\} \cup \{(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; \varnothing 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)(U,V) is a separation of LL: both open and nonempty, disjoint, with UV=LU \cup V = L.

assume-contraA4
2.1

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

step 1.1A1
3.1

Put S:={tU:atb}S := \{\, t \in U : a \le t \le b \,\}. It is nonempty, containing aa, and bb is an upper bound of it, so c:=supSc := \sup S exists by [A2] and satisfies acba \le c \le b, since aSa \in S and bb is an upper bound.

step 2.1A2
4.1

Suppose cVc \in V. Then cac \ne a, since aUa \in U and the two sets are disjoint, so a<ca < c by [A1] and aca \le c. By [A3] there is a basic open WW with cWVc \in W \subseteq V; WW is neither LL nor a set L<qL_{<q}, since either would contain aa, giving aVa \in V. So WW is L>pL_{>p} or (p,q)(p,q) with p<cp < c, and in both cases (p,c]WV(p, c] \subseteq W \subseteq V.

step 1.1step 3.1A1A3
4.2

Suppose instead cUc \in U. Then cbc \ne b, so c<bc < b by [A1] and cbc \le b. By [A3] there is a basic open WW with cWUc \in W \subseteq U; WW is neither LL nor a set L>pL_{>p}, since either would contain bb, giving bUb \in U. So WW is L<qL_{<q} or (p,q)(p,q) with c<qc < q, and in both cases [c,q)WU[c, q) \subseteq W \subseteq U; moreover qbq \le b, since bUb \notin U and c<bc < b would otherwise put bb in [c,q)[c,q).

step 1.1step 3.1A1A3
5.1

In the case of step 4.1, p<c=supSp < c = \sup S, so pp is not an upper bound of SS by [A2] and there is sSs \in S with p<scp < s \le c; then s(p,c]Vs \in (p,c] \subseteq V and sUs \in U, contradicting UV=U \cap V = \varnothing.

step 1.1step 3.1step 4.1A2
5.2

In the case of step 4.2, order-density gives zz with c<z<qc < z < q by [A2]; then z[c,q)Uz \in [c,q) \subseteq U, and ac<z<qba \le c < z < q \le b, so zSz \in S while z>c=supSz > c = \sup S, contradicting that supS\sup S is an upper bound of SS.

step 3.1step 4.2A2
6.1

By step 1.1 the point cc lies in UV=LU \cup V = L, so one of the two cases applies, and each is contradictory by steps 5.1 and 5.2. Hence no separation of LL exists and LL is connected; this is claim 1.

step 1.1step 5.1step 5.2A4
7.1

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

step 6.1A2A4A5discharge-contradiction

Remarks

  • Both hypotheses are spent, each exactly once. The least upper bound property produces cc at step 3.1, and order-density produces the point zz at step 5.2. Neither may be dropped. An ordered set with a jump, a pair x<yx < y with (x,y)=(x,y) = \varnothing, is separated by the two open sets L<yL_{<y} and L>xL_{>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}\{q : q^2 < 2 \text{ or } q < 0\} and its complement, both open.

  • Why the argument is asymmetric between the two cases. Case 4.1 needs only that cc is a least upper bound; case 4.2 needs a point strictly above cc inside UU, 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 CC 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 67 results over 14 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