Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)judge 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\mathbb{R}: the nine order-convex forms, nondegeneracy, and length

Definition

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

A subset IRI \subseteq \mathbb{R} is order-convex when

x,yI and xzy    zI.x, y \in I \text{ and } x \le z \le y \;\Longrightarrow\; z \in I .

The intervals of R\mathbb{R} are the sets of the following nine forms, where a,bRa, b \in \mathbb{R}:

bounded formsone-sided and full forms
(a,b)(a,b){x:a<x<b}\{x : a < x < b\}(a,)(a,\infty){x:a<x}\{x : a < x\}
[a,b][a,b]{x:axb}\{x : a \le x \le b\}[a,)[a,\infty){x:ax}\{x : a \le x\}
[a,b)[a,b){x:ax<b}\{x : a \le x < b\}(,b)(-\infty,b){x:x<b}\{x : x < b\}
(a,b](a,b]{x:a<xb}\{x : a < x \le b\}(,b](-\infty,b]{x:xb}\{x : x \le b\}
(,)(-\infty,\infty)R\mathbb{R}

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

The symbols ±\pm\infty are notation and not elements of R\mathbb{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 xx alone, and no arithmetic is ever performed with \infty. This is the same refusal to extend R\mathbb{R} silently that Conventions: sup\sup \emptyset, 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<xa < x, axa \le x, x<bx < b or xbx \le b, and each such condition is inherited by an intermediate point: if a<xa < x and xzx \le z then a<za < z, and if zyz \le y and y<by < b then z<bz < b, by transitivity of the order (Ordered field). Applying this to whichever one or two conditions define the form in question gives zIz \in I whenever x,yIx, y \in I and xzyx \le z \le 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, aa is a lower bound and bb an upper bound. The other five forms are unbounded, on the side or sides written with \infty; 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 aa and bb:

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

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

Closed bounded intervals. These are the sets [a,b][a,b] with aba \le 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 aba \le b in this library.

Length. The length of a bounded interval presented by its endpoints aba \le b is

=ba    0.\ell = b - a \;\ge\; 0 .

Length is attached to the presentation by endpoints and is not recovered from the set: (a,b)(a,b), [a,b)[a,b) and (a,b](a,b] are all empty when a=ba = b, and so is (c,c)(c,c) for any other cc, while each of these presentations has length 00, 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,)[a,\infty) and suppose uRu \in \mathbb{R} were an upper bound of it. The element x=a+ua+1x = a + |u - a| + 1 satisfies xax \ge a, so x[a,)x \in [a,\infty), and xa+(ua)+1=u+1>ux \ge a + (u - a) + 1 = u + 1 > u, since tt|t| \ge t (Basic properties of the absolute value) and 1>01 > 0 (The multiplicative identity is positive). That contradicts xux \le u. The same computation with aa replaced by any element of (a,)(a,\infty) handles the open form, and reflecting through the origin handles (,b)(-\infty,b) and (,b](-\infty,b]; R\mathbb{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\mathbb{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}[a,a] = \{a\} and (a,a)=(a,a) = \emptyset 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][a,a], which is exactly the single point.

Depends on

Used by

…and 305 more results.

Dependency tree · next 3 levels

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