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
- Cut time does not exceed first conjugate time 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
- Chebyshev constant of a compact planar set Definition
- Compact-box global minimization problems Definition
- Fekete points and the transfinite diameter of a compact set 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
- Kazhdan pairs, Kazhdan sets and Kazhdan constants 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
- Robin constant and logarithmic capacity of a compact set 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 likelihood-ratio threshold with boundary randomization exists Lemma
- A normal sequence of entourages yields a uniformly continuous pseudometric with controlled dyadic balls Lemma
- A randomized threshold attains every test size Lemma
- A strong Wolfe step exists on a bounded-below descent ray Lemma
- Bounded bowl-shaped losses have Gaussian-centered Lipschitz minorants Lemma
- Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces Lemma
- Closed witness codings and completion measurability of Borel projections 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
- Monotonicity of the Fekete diameters and the transfinite diameter Lemma
…and 30 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)