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.
Greatest lower bound (infimum)
Definition
Let and . Then is a greatest lower bound, or infimum, of if both of the following hold:
- is a lower bound of (Lower bound, bounded below, bounded set), that is, for every ;
- for every lower bound of .
Written out in one line:
An infimum, when it exists, is unique (Suprema and infima are unique), so we may write for it.
Remarks
- This is the exact dual of the least upper bound (supremum) of Complete ordered field (least-upper-bound property): reverse every inequality and swap "least" for "greatest". The two notions are related by reflection through (Reflection through zero exchanges upper and lower bounds).
- Existence is deliberately not part of the definition. That every nonempty subset of which is bounded below actually has an infimum is a theorem, Every nonempty set bounded below has an infimum, derived from the least-upper-bound property; it is not an axiom and it is not free.
- As with a supremum, an infimum need not belong to ; when it does, it is the minimum of (Maximum and minimum of a set).
- The usable form of the definition in later arguments is the epsilon characterisation Epsilon characterisation of the infimum: exactly when is a lower bound that cannot be raised by any positive amount without losing that property.
Depends on
Used by
- Compact operator iff approximation numbers tend to zero Corollary
- Cut time does not exceed first conjugate time Corollary
- Strict convexity gives uniqueness of a minimiser Corollary
- The index of a cycle is locally constant off its trace and vanishes far from it Corollary
- 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
- Positive sectional curvature with no fixed lower bound on a noncompact manifold Counterexample
- The Dirichlet function on [0,1] has lower Darboux integral 0 and upper Darboux integral 1, so it is bounded and not Riemann integrable Counterexample
- The indicator of the Smith-Volterra-Cantor set is discontinuous exactly on a nowhere dense set, and is not Riemann integrable, because that set does not have measure zero 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
- Certified lower, upper, and emptiness bounds on a box 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
- Half-relaxed limits of a locally bounded family Definition
- Jordan inner and outer content and Jordan measurable bounded sets in ℝᵐ Definition
- Kazhdan pairs, Kazhdan sets and Kazhdan constants 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
- Oscillation of a real function on subsets of ℝᵐ and at a point Definition
- Proper, coercive and weakly lower semicontinuous extended-real functionals Definition
- Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral Definition
- The Hopf--Lax operator and the Hopf--Lax formula 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
- The oscillation ω_f(S) = sup{ |f(x) - f(y)| : x, y ∈ S } of f on a set and the oscillation ω_f(c) = inf_δ > 0 ω_f(A ∩ N_δ(c)) at a point, both taken in the extended reals Definition
- Trace class operator Definition
- Upper and lower semicontinuous envelopes by local limsup and liminf Definition
- ∫₀¹ x² = 1/3, computed from the Darboux definition with uniform partitions and the closed form ∑_k<n k² = n(n-1)(2n-1)/6 Example
- ∫₀³ ⌊ x ⌋ = 3: the floor function is nondecreasing, hence integrable, and the integral is computed from the uniform partitions Example
- A step function integrated by additivity over subintervals, and the same value from the definition Example
- Distance hessian in euclidean space Example
- Every nonempty closed subset A of ℝ is the zero set of x ↦ d(x, A) and the intersection of the open sets {x : d(x,A) < 1/(n+1)}, worked for [0,1] and for {0} Example
- inf{1/n : n ≥ 1} = 0, not attained, while sup{1/n : n ≥ 1} = 1 is Example
- One refinement worked out for f(x) = x² on [0,1]: adding the point 1/2 to the trivial partition raises the lower sum from 0 to 1/8 and lowers the upper sum from 1 to 5/8 Example
- sup(0,1) = 1 and inf(0,1) = 0, with neither attained Example
…and 64 more results.
Dependency tree · two levels
2 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)
- 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)