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 subset of is connected if and only if it is order-convex, that is, an interval
Statement
Let . Then is connected (Separated sets, disconnection, and connected subset of ) if and only if is order-convex (Intervals of : the nine order-convex forms, nondegeneracy, and length), that is, if and only if
On the word "interval". Order-convexity is exactly the defining property that Intervals of : the nine order-convex forms, nondegeneracy, and length proves for each of its nine forms, and in that sense the theorem says that the connected subsets of are the intervals. The converse classification, that every order-convex subset of is empty or one of the nine forms, is true and is explicitly not proved anywhere in this library; Intervals of : the nine order-convex forms, nondegeneracy, and length records that omission in its own remarks. So the statement proved below is the equivalence with order-convexity, and the phrase "is an interval" is to be read as "is order-convex" throughout this page.
Facts & Assumptions
Given: A subset .
Separated sets, disconnection, connectedness; separated sets are disjoint (Separated sets, disconnection, and connected subset of ).
is the smallest closed superset of , so gives and for every closed ; and is exactly the set of points every neighbourhood of which meets (The closure equals the set together with its limit points, equals the set of points every neighbourhood of which meets it, and is the smallest closed superset; a set is closed iff it contains its limit points, Interior, closure, boundary and exterior of a subset of ).
Order-convexity, and the interval forms: and are closed sets, and are open sets, and the order is total and transitive (Intervals of : the nine order-convex forms, nondegeneracy, and length, Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Ordered field, Complete ordered field (least-upper-bound property)).
Least-upper-bound property: a nonempty subset of bounded above has a unique least upper bound (Complete ordered field (least-upper-bound property), Suprema and infima are unique, Lower bound, bounded below, bounded set).
Epsilon characterisation: for nonempty bounded above and , every admits with (Epsilon characterisation of the supremum).
Every nonempty finite set of reals has a minimum, which is one of its members (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).
Ordered-field arithmetic: , so and ; for one has ; adding a constant preserves an inequality (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.
Proof
Suppose is not order-convex: there are and with and ; then and , so . Put and ; then and , so both are nonempty, and because no element of equals .
Suppose instead that is order-convex and that is a disconnection of ; fix and . Separated sets are disjoint by [L1], so , and interchanging the names and if necessary, which is legitimate because the hypotheses on the pair are symmetric, we may assume .
For a nonempty bounded above, : for every real the fact [L5] supplies with , so and ; thus every neighbourhood of meets , and [L2] gives .
In the situation of step 1.1 the pair is a disconnection: is a closed set containing , so by [L2], whence ; symmetrically and . So and are separated, nonempty, and their union is , and is disconnected.
In the situation of step 1.2 put ; it is nonempty because and , and it is bounded above by , so exists by [L4], and since and is an upper bound.
: from and [L2] we get , and by step 1.3, so and hence because ; on the other hand with and order-convex gives , so .
, since and are distinct by [L1] while ; and every with lies in : such a satisfies , so by order-convexity, and , for otherwise would force .
, which is impossible: given a real , put , a positive real by [L7] and [L8] since , and ; then and , so by step 4.1, while , so . Hence every neighbourhood of meets and by [L2]; but by step 3.1 and by [L1]. So the assumed disconnection cannot exist and an order-convex is connected.
Step 2.1 shows that a set which is not order-convex is disconnected, hence a connected set is order-convex; step 5.1 shows that an order-convex set admits no disconnection, hence is connected. The two together are the asserted equivalence.
Remarks
-
Where completeness is spent. Only in step 2.2, which produces ; no other step uses the least-upper-bound property, and the rest is the order, ordered-field arithmetic and the definition of separation. The obstruction over an incomplete ordered field is traceable to the failure of that supremum to exist, and it is visible in is bounded and disconnected, so being an interval of is not enough ↗: the set contains all the rationals between its endpoints and is nevertheless disconnected as a subset of , split at an irrational point that does not see.
-
The two directions are of different characters. "Not order-convex implies disconnected" is a construction, step 1.1, and needs nothing beyond the order. "Order-convex implies connected" is where the work sits, and the supremum produced in step 2.2 is the point at which the two pieces would have to meet; the contradiction is that it is adherent to both.
-
The theorem is about subsets of and its statement is written in order vocabulary, so it cannot even be stated where no order is present; Which results on this page use the order of and therefore have no general-topological analogue collects the results on this page with that feature.
Depends on
Separated sets, disconnection, and connected subset of
Intervals of : the nine order-convex forms, nondegeneracy, and length
Complete ordered field (least-upper-bound property)
Epsilon characterisation of the supremum
Suprema and infima are unique
Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen
Lower bound, bounded below, bounded set
The closure equals the set together with its limit points, equals the set of points every neighbourhood of which meets it, and is the smallest closed superset; a set is closed iff it contains its limit points
Interior, closure, boundary and exterior of a subset of
The -neighbourhood and the punctured -neighbourhood of a point of
Every nonempty finite set of reals has a maximum and a minimum
Maximum and minimum of a set
Ordered field
Order is preserved by adding a constant and by adding inequalities
The multiplicative identity is positive
Sign rules for products and monotonicity of multiplication