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.
Suprema and infima are unique
Statement
Let . If and are both least upper bounds of (Complete ordered field (least-upper-bound property)), then . If and are both greatest lower bounds of (Greatest lower bound (infimum)), then .
Consequently a set has at most one supremum and at most one infimum, and the notations and denote single, well-determined real numbers whenever they exist.
Facts & Assumptions
Given: A subset of the complete ordered field , together with elements .
is a least upper bound of exactly when is an upper bound of and for every upper bound of (Complete ordered field (least-upper-bound property)).
is a greatest lower bound of exactly when is a lower bound of and for every lower bound of (Greatest lower bound (infimum)).
Antisymmetry of the order: for , if and then . This is trichotomy in the underlying ordered field, which says that exactly one of , , holds, so, reasoning by contradiction, would put both and in force, which trichotomy forbids (Complete ordered field (least-upper-bound property), Ordered field).
Proof
Assume and are both least upper bounds of ; in particular each of them is an upper bound of and each is every upper bound of .
Assume and are both greatest lower bounds of ; in particular each of them is a lower bound of and each is every lower bound of .
Applying the leastness of to the upper bound gives , and applying the leastness of to the upper bound gives .
Applying the greatestness of to the lower bound gives , and applying the greatestness of to the lower bound gives .
By antisymmetry and , so a least upper bound and a greatest lower bound of are each unique when they exist, which is what licenses writing and .
Depends on
Used by
- Every nondegenerate interval of ℝ is uncountable Corollary
- Refuted: convergence uniformly on every compact subset of ℝ implies uniform convergence. The maps x ↦ x/(n+1) separate the two Counterexample
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space Definition
- Bounded variation and total variation on an interval Definition
- For bounded f on [a,b] and a partition P: the infimum mᵢ and supremum Mᵢ of f on the i-th subinterval, and the lower and upper Darboux sums L(f,P) = ∑ᵢ mᵢ Δᵢ and U(f,P) = ∑ᵢ Mᵢ Δᵢ Definition
- Jordan inner and outer content and Jordan measurable bounded sets in ℝᵐ Definition
- Lower and upper Darboux sums over a grid partition in ℝᵐ Definition
- The Cantor function on [0,1], defined on the Cantor set through ternary digits and extended constantly across each removed interval Definition
- The lower and upper Darboux integrals of a bounded f on [a,b] as sup_P L(f,P) and inf_P U(f,P), Darboux integrability as their equality, and the notation ∫ₐᵇ f Definition
- The lower and upper Darboux integrals over a nondegenerate rectangle in ℝᵐ Definition
- 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 Definition
- C([0,1], ℝ) is complete, and on it the uniform metric and the supremum metric induce the same topology Example
- min(|x-y|, 1) on ℝ has the usual topology and diameter at most 1 Example
- The moving spikes on [0,1] converge pointwise to 0, do not converge uniformly, and do not converge in the topology of compact convergence Example
- The supremum metric d_∞(f,g) = supₓ |f(x) - g(x)| on the bounded real-valued functions on a set Example
- Convergence in the uniform metric is exactly uniform convergence: one N serving every point Lemma
- Epsilon characterisation of the supremum Lemma
- For a nonempty set X and a metric space (Y,d) the uniform metric barρ(f,g) = supₓ min{d(f(x),g(x)), 1} is a metric on Y^X Lemma
- min(d,1) and d/(1+d) are metrics uniformly equivalent to d, so every metric space carries a bounded metric with the same topology Lemma
- Monotonicity of the supremum under inclusion Lemma
- The supremum is attained exactly when a maximum exists Lemma
- The supremum metric d_∞(f,g) = supₓ |f(x) - g(x)| is a metric on the bounded real-valued functions on a nonempty set Lemma
- Total variation is additive over adjacent subintervals and decreases under restriction Lemma
- Conventions: sup ∅, unbounded sets, and the extended reals Remark
- A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to 0 Theorem
- A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum Theorem
- A subset of ℝ is connected if and only if it is order-convex, that is, an interval Theorem
- Dini's theorem: on a compact metric space a nondecreasing sequence of continuous real functions converging pointwise to a continuous limit converges uniformly Theorem
- Every nonempty set bounded below has an infimum Theorem
- Every open subset of ℝ is a countable disjoint union of open intervals, namely its order components Theorem
- Existence and uniqueness of n-th roots: a unique a^1/n ≥ 0 with (a^1/n)ⁿ = a Theorem
- If (Y,d) is complete then Y^X is complete in the uniform metric, and so is C(X,Y) Theorem
- Integrable functions on [a,b] form a set closed under sums and scalar multiples, and ∫ₐᵇ(λ f+μ g) = λ∫ₐᵇ f + μ∫ₐᵇ g Theorem
- ℝ is uncountable (Cantor's nested intervals, 1874) Theorem
- The Cantor function is well defined, satisfies c(x) ≤ c(y) whenever x ≤ y, is surjective onto [0,1], and is constant on every interval removed from the Cantor set Theorem
- The long ray is a linear continuum, hence connected; every one of its at most countable subsets is bounded above, assuming countable choice Theorem
Cited to discharge well-definedness by Greatest lower bound (infimum).
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 5 results over 5 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
- Infimum and supremum (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)