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.
Every nonempty set bounded below has an infimum
Statement
Let be nonempty and bounded below. Then has a greatest lower bound in (Greatest lower bound (infimum)), and it is given by
In particular the complete ordered field has the greatest-lower-bound property, which is therefore not an extra axiom: it is a consequence of the least-upper-bound property.
Facts & Assumptions
Given: A nonempty that is bounded below, and its reflection .
The least-upper-bound property of : every nonempty subset of that is bounded above has a least upper bound in , namely an upper bound that is every upper bound (Complete ordered field (least-upper-bound property)).
Reflection: ; is nonempty exactly when is; is an upper bound of a set exactly when is a lower bound of ; and is a lower bound of exactly when is an upper bound of (Reflection through zero exchanges upper and lower bounds).
Greatest lower bound (infimum): is one for when is a lower bound of and for every lower bound of (Greatest lower bound (infimum)).
A least upper bound and a greatest lower bound are unique when they exist, so the notations and are unambiguous (Suprema and infima are unique).
Negation reverses the order, elementwise: , because and additive inverses are unique (Field, Identities and inverses in a field are unique); and if and only if , because translation invariance applied with the constant turns into and, applied with the constant , turns back into , while holds exactly when (Order is preserved by adding a constant and by adding inequalities).
Proof
By hypothesis and is bounded below; fix a lower bound of , so for every .
Let be an arbitrary lower bound of ; then is an upper bound of .
Since is nonempty, so is , and since is a lower bound of , its negative is an upper bound of ; hence is a nonempty subset of that is bounded above.
By the least-upper-bound property, has a least upper bound in ; write , which is well defined by uniqueness.
Define .
The element is the least of the upper bounds of and is one of them, hence .
Apply the reflection fact to the set : since is an upper bound of , its negative is a lower bound of , and ; so is a lower bound of .
Negating the inequality reverses it, giving , that is .
Thus is a lower bound of satisfying for every lower bound of , so is a greatest lower bound of ; it is the only one, so exists and .
Remarks
- The theorem is not a restatement of the least-upper-bound property: it is proved from it, by transporting the problem across the order-reversing bijection of Reflection through zero exchanges upper and lower bounds. Nothing about beyond the complete-ordered-field axioms is used.
- The hypotheses are both needed. The empty set is bounded below by every real and has no greatest lower bound, and a set unbounded below has no lower bound at all; the dual failures for suprema are recorded in FALSE: every subset of has a supremum.
- The identity is the standard device for turning any statement about suprema into its dual; Epsilon characterisation of the infimum is the first application on this page.
Depends on
Used by
- Compact operator iff approximation numbers tend to zero Corollary
- The index of a cycle is locally constant off its trace and vanishes far from it Corollary
- 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
- ℤ and {n + 1/n : n ≥ 2} are disjoint closed subsets of ℝ at distance 0, so the set-to-set distance is not a metric Counterexample
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space 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
- Levy prokhorov metric Definition
- Limit superior and limit inferior of a real sequence as infₙ sup_k ≥ n xₖ and supₙ inf_k ≥ n xₖ in ℝ̄ Definition
- Lower and upper Darboux sums over a grid partition in ℝᵐ Definition
- Minkowski gauge for an open convex zero-neighborhood Definition
- Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral Definition
- The finite gauge of an open convex neighbourhood of zero 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
- Norm-attaining functionals on a Hilbert space Example
- sup(0,1) = 1 and inf(0,1) = 0, with neither attained Example
- |d(x,A) - d(y,A)| ≤ d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz Lemma
- A bounded separately holomorphic function on a polydisc is Lipschitz on every smaller polydisc Lemma
- A closed L2 subspace with trivial orthogonal complement fills L2 Lemma
- A contour missing a point subdivides into arcs lying in discs that miss it Lemma
- A normal sequence of entourages yields a uniformly continuous pseudometric with controlled dyadic balls Lemma
- Continuity, sublinearity and strict sublevels of an open convex gauge Lemma
- Epsilon characterisation of the infimum Lemma
- Every subset of ℝ̄ has a least upper bound and a greatest lower bound in ℝ̄, agreeing with the real supremum and infimum on nonempty sets bounded in ℝ Lemma
- If (Uᵣ)_r ∈ D are open with Uᵣ ⊆ Uₛ whenever r < s and U₁ = X, then x ↦ inf{ r ∈ D : x ∈ Uᵣ } is a continuous map X → [0,1], and no choice principle is used Lemma
- James convex-block norm-attainment criterion Lemma
- Quantitative Bishop–Phelps support functional construction Lemma
- Refining a partition raises the lower Darboux sum and lowers the upper one, and every lower sum is at most every upper sum: L(f,P) ≤ L(f,P') ≤ U(f,P') ≤ U(f,P) when P' refines P, and L(f,P) ≤ U(f,Q) for arbitrary partitions P and Q; moreover the two changes are at most 2M(n' - n)‖P‖ Lemma
- Singular values equal approximation numbers Lemma
- Supremum of a scalar multiple Lemma
- Uniform convexity gives unique asymptotic centers 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
- Continuous separation when one convex set is open Theorem
- Darboux criterion for Riemann–Stieltjes integrability with a nondecreasing integrator Theorem
- Every open subset of ℝ is a countable disjoint union of open intervals, namely its order components Theorem
- Extreme value theorem: a continuous real function on a nonempty compact subset of ℝ attains a greatest and a least value Theorem
- Hilbert spaces are reflexive by Riesz representation Theorem
…and 7 more results.
Dependency tree · two levels
9 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
- Infimum and supremum (Wikipedia) (standard reference, not scraped)
- Least-upper-bound property (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)
- MIT 18.100A, Complete Lecture Notes (standard reference, not scraped)