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 : the nine order-convex forms, nondegeneracy, and length
Definition
Throughout, is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field) with its order (Order on the reals).
A subset is order-convex when
The intervals of are the sets of the following nine forms, where :
| bounded forms | one-sided and full forms | ||
|---|---|---|---|
An interval is open when both of its written endpoints are excluded, that is for the forms , , and ; it is closed when both written endpoints are included, that is for , , and . The forms and are half-open.
The symbols are notation and not elements of . They mark which side carries no endpoint condition at all; the five forms in the right column are defined by the displayed conditions on alone, and no arithmetic is ever performed with . This is the same refusal to extend silently that Conventions: , 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 , , or , and each such condition is inherited by an intermediate point: if and then , and if and then , by transitivity of the order (Ordered field). Applying this to whichever one or two conditions define the form in question gives whenever and .
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, is a lower bound and 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 and :
- is nonempty exactly when , and it is nondegenerate exactly when . It is the singleton when .
- , and are nonempty exactly when , and then each is nondegenerate.
The only assertion here that is not immediate from the defining conditions is that makes nonempty with at least two points. It holds because , which follows from by adding , respectively , to both sides and halving (Ordered field); repeating the halving inside produces a second point.
Closed bounded intervals. These are the sets with , 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 in this library.
Length. The length of a bounded interval presented by its endpoints is
Length is attached to the presentation by endpoints and is not recovered from the set: , and are all empty when , and so is for any other , while each of these presentations has length , 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 and suppose were an upper bound of it. The element satisfies , so , and , since (Basic properties of the absolute value) and (The multiplicative identity is positive). That contradicts . The same computation with replaced by any element of handles the open form, and reflecting through the origin handles and ; 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 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. and 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 , which is exactly the single point.
Depends on
Used by
- A bounded function on [a,b] whose set of discontinuities is at most countable is Riemann integrable Corollary
- A function continuous on an interval I whose derivative vanishes at every interior point of I is constant on I; consequently two such functions with the same derivative differ by a constant Corollary
- A real-valued continuous map on a connected space has order-convex image, so it takes every value between any two of its values Corollary
- Every continuous function on an interval has a primitive; two primitives differ by a constant; and ∫ₐᵇ f = G(b)-G(a) for any primitive G Corollary
- If f : [a,b] → ℝᵐ is differentiable with integrable f' then ∫ₐᵇ f' = f(b)-f(a); and a bounded derivative makes f Lipschitz Corollary
- If f is continuous on an interval I and |f'| ≤ M at every interior point, then |f(x) - f(y)| ≤ M|x-y| for all x,y ∈ I, so f is Lipschitz with constant M and uniformly continuous on I Corollary
- If f,g are integrable on [a,b] then so are | f|, f², fg, max(f,g) and min(f,g), and |∫ₐᵇ f| ≤ ∫ₐᵇ| f| Corollary
- Polynomials are uniformly dense in C([a,b],ℝ) for every closed interval Corollary
- The Cantor function is continuous on [0,1] Corollary
- The connected subspaces of ℝ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in ℝ" Corollary
- The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval Corollary
- The mean value theorem, as the case g(x) = x of Cauchy's: for f continuous on [a,b] with a < b and differentiable on (a,b) there is c ∈ (a,b) with f(b) - f(a) = f'(c)(b-a) Corollary
- Under dependent choice, a continuous real-valued map on a closed subspace of a normal space extends to the whole space, and a map into an open interval extends into that same open interval Corollary
- [0,1) is neither open nor closed in ℝ Counterexample
- {0} ∪ [1,2] is closed, has an isolated point, and is not perfect Counterexample
- ⋂ₖ (-1/k, 1/k) = {0} is not open Counterexample
- 1/4 lies in the Cantor set and is the endpoint of no removed interval, so the endpoints do not exhaust it Counterexample
- A continuous injection on [0,1] ∪ [2,3] that is not monotone, so the interval hypothesis cannot be dropped from the strict-monotonicity theorem Counterexample
- A curve for which the mean value inequality is an equality, showing the constant cannot be improved Counterexample
- A function differentiable on [0,1] whose derivative is unbounded, hence not Riemann integrable Counterexample
- A function that is not Riemann integrable although | f| is Counterexample
- An upper semicontinuous function on [0,1] that is bounded below and attains no minimum, so the semicontinuous extreme value theorem is genuinely one-sided Counterexample
- Collapsing the set of naturals inside ℝ to a point gives a quotient of ℝ that is not locally compact at the collapsed point Counterexample
- Continuous f and integrable sign-changing g with ∫ₐᵇ fg ≠ f(ξ)∫ₐᵇ g for every ξ Counterexample
- Continuous fₙ → 0 pointwise on [0,1] with ∫₀¹ fₙ = 1 for every n Counterexample
- f(t) = (t², t³) on [0,1]: no ξ satisfies f(1)-f(0) = f'(ξ) Counterexample
- f(x) = x on [0,1) with f(1) = 0 is differentiable at every point of (0,1) with f' ≡ 1, yet no c satisfies f(1) - f(0) = f'(c), so continuity on the closed interval cannot be dropped from the mean value theorem Counterexample
- For the Dirichlet function every uniform partition with rational tags gives Riemann sum 1, so the sums converge along that sequence of tagged partitions although the function is not integrable: the mesh condition of the Riemann definition quantifies over all tagged partitions and cannot be weakened to one sequence Counterexample
- In {0} ∪ [1,2] with the metric of ℝ, the closure of B(0,1) = {0} is {0} while the closed ball is {0,1} Counterexample
- In ℝ the interiors of ℚ and of its complement are both empty while the interior of their union is everything Counterexample
- In the cocountable topology on ℝ the sequential closure of [0,1] is [0,1] while its closure is all of ℝ Counterexample
- In the K-topology on ℝ the closed set K ∪ {0} carries a continuous two-valued function with no continuous extension Counterexample
- In the subspace of ℝ² made of the vertical unit segments over 1/(n+1) together with the two points (0,0) and (0,1), the component of (0,0) is a singleton while its quasicomponent is {(0,0), (0,1)} Counterexample
- Integrable φ and integrable f with φ∘ f not integrable: the order of the hypotheses in the composition theorem cannot be reversed Counterexample
- On (0,∞) the metrics |x-y| and |1/x - 1/y| have the same topology and are not uniformly equivalent Counterexample
- On (0,∞) the metrics |x-y| and |1/x - 1/y| share their topology and not their Cauchy sequences Counterexample
- On (0,1) the identity is bounded with no greatest value and x ↦ 1/x is continuous and unbounded, so the extreme value theorem needs compactness and not merely boundedness of the domain Counterexample
- On A = ([0,∞) × ℝ) ∪ (ℝ × {0}) the first projection is a quotient map, by the section x ↦ (x,0), and is neither open nor closed Counterexample
- On the domain {0} ∪ [1,2] every real is vacuously a limit at 0 Counterexample
- ℚ ∩ [0,1] has measure zero and not content zero, although it is bounded Counterexample
…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
- Interval (mathematics) (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (segments and cells) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §0.3 and §1.1 (standard reference, not scraped)