Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-26
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.

Intervals of R: the nine order-convex forms, nondegeneracy, and length

Definition

Throughout, R is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field) with its order (Order on the reals).

A subset I⊆R is order-convex when

x,y∈I and x≤z≤y  ⟹  z∈I.

The intervals of R are the sets of the following nine forms, where a,b∈R:

bounded formsone-sided and full forms
(a,b){x:a<x<b}(a,∞){x:a<x}
[a,b]{x:a≤x≤b}[a,∞){x:a≤x}
[a,b){x:a≤x<b}(−∞,b){x:x<b}
(a,b]{x:a<x≤b}(−∞,b]{x:x≤b}
(−∞,∞)R

An interval is open when both of its written endpoints are excluded, that is for the forms (a,b), (a,∞), (−∞,b) and (−∞,∞); it is closed when both written endpoints are included, that is for [a,b], [a,∞), (−∞,b] and (−∞,∞). The forms [a,b) and (a,b] are half-open.

The symbols ±∞ are notation and not elements of R. They mark which side carries no endpoint condition at all; the five forms in the right column are defined by the displayed conditions on x alone, and no arithmetic is ever performed with ∞. This is the same refusal to extend R silently that Conventions: sup⁡∅, unbounded sets, and the extended reals records for suprema.

Every one of the nine forms is order-convex. Each is defined by a conjunction of at most two conditions, each of the shape a<x, a≤x, x<b or x≤b, and each such condition is inherited by an intermediate point: if a<x and x≤z then a<z, and if z≤y and y<b then z<b, by transitivity of the order (Ordered field). Applying this to whichever one or two conditions define the form in question gives z∈I whenever x,y∈I and x≤z≤y.

Bounded intervals. An interval is bounded (Lower bound, bounded below, bounded set) exactly when it is of one of the four forms in the left column: for those, a is a lower bound and b an upper bound. The other five forms are unbounded, on the side or sides written with ∞; the verification is in the remarks below.

Nondegeneracy. An interval is degenerate when it has at most one element, and nondegenerate when it has at least two. For the four bounded forms with endpoints a and b:

  • [a,b] is nonempty exactly when a≤b, and it is nondegenerate exactly when a<b. It is the singleton {a} when a=b.
  • (a,b), [a,b) and (a,b] are nonempty exactly when a<b, and then each is nondegenerate.

The only assertion here that is not immediate from the defining conditions is that a<b makes (a,b) nonempty with at least two points. It holds because a<(a+b)/2<b, which follows from a<b by adding a, respectively b, to both sides and halving (Ordered field); repeating the halving inside (a,(a+b)/2) produces a second point.

Closed bounded intervals. These are the sets [a,b] with a≤b, which is exactly the condition making them nonempty. They are the intervals the nested interval property is stated for, and the phrase closed bounded interval always carries the hypothesis a≤b in this library.

Length. The length of a bounded interval presented by its endpoints a≤b is

ℓ=b−a  ≥  0.

Length is attached to the presentation by endpoints and is not recovered from the set: (a,b), [a,b) and (a,b] are all empty when a=b, and so is (c,c) for any other c, while each of these presentations has length 0, so nothing inconsistent arises; but the endpoints are named explicitly at every point where a length is used in this library, and never inferred from the set. Unbounded intervals are assigned no length.

Remarks

  • Why the five unbounded forms really are unbounded. Take [a,∞) and suppose u∈R were an upper bound of it. The element x=a+∣u−a∣+1 satisfies x≥a, so x∈[a,∞), and x≥a+(u−a)+1=u+1>u, since ∣t∣≥t (Basic properties of the absolute value) and 1>0 (The multiplicative identity is positive). That contradicts x≤u. The same computation with a replaced by any element of (a,∞) handles the open form, and reflecting through the origin handles (−∞,b) and (−∞,b]; R itself is unbounded on both sides for the same reason. Note that this uses no Archimedean property: it is the failure of a single bound, not the cofinality of the naturals.

  • The converse classification is not asserted here. It is true that every order-convex subset of R is empty or one of the nine forms, and the proof runs through suprema and infima, but nothing in this library needs it and it is not proved anywhere here. What is used is only the direction proved above: each of the nine forms is order-convex.

  • Degenerate intervals are kept, not excluded. [a,a]={a} and (a,a)=∅ are intervals under this definition. Excluding them would force a nonemptiness hypothesis into every statement that produces an interval, and the nested interval property is a good illustration: its conclusion is that the intersection is nonempty, and in the equality case the intersection is the degenerate interval [a,a], which is exactly the single point.

Depends on

Used by

…and 346 more results.

Dependency tree · two levels

7 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