TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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 $S \subseteq \mathbb{R}$ be nonempty and bounded below. Then $S$ has a greatest lower bound in $\mathbb{R}$ (Greatest lower bound (infimum)), and it is given by

$\inf S = -\sup(-S), \qquad \text{where } -S = \{-s : s \in S\}.$

In particular the complete ordered field $\mathbb{R}$ 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 $S \subseteq \mathbb{R}$ that is bounded below, and its reflection $-S = \{-s : s \in S\}$ .

[L1]

The least-upper-bound property of $\mathbb{R}$ : every nonempty subset of $\mathbb{R}$ that is bounded above has a least upper bound in $\mathbb{R}$ , namely an upper bound that is $\le$ every upper bound (Complete ordered field (least-upper-bound property)).

[L2]

Reflection: $-(-S) = S$ ; $S$ is nonempty exactly when $-S$ is; $u$ is an upper bound of a set $X$ exactly when $-u$ is a lower bound of $-X$ ; and $\ell$ is a lower bound of $X$ exactly when $-\ell$ is an upper bound of $-X$ (Reflection through zero exchanges upper and lower bounds).

[L3]

Greatest lower bound (infimum): $\ell$ is one for $S$ when $\ell$ is a lower bound of $S$ and $\ell' \le \ell$ for every lower bound $\ell'$ of $S$ (Greatest lower bound (infimum)).

[L4]

A least upper bound and a greatest lower bound are unique when they exist, so the notations $\sup$ and $\inf$ are unambiguous (Suprema and infima are unique).

[L5]

Negation reverses the order, elementwise: $-(-a) = a$ , because $(-a) + a = 0$ and additive inverses are unique (Field, Identities and inverses in a field are unique); and $a \le b$ if and only if $-b \le -a$ , because translation invariance applied with the constant $-a - b$ turns $a < b$ into $-b < -a$ and, applied with the constant $a + b$ , turns $-b < -a$ back into $a < b$ , while $a = b$ holds exactly when $-a = -b$ (Order is preserved by adding a constant and by adding inequalities).

Proof

technique · direct

1.1

By hypothesis $S \ne \emptyset$ and $S$ is bounded below; fix a lower bound $\ell_0$ of $S$ , so $\ell_0 \le s$ for every $s \in S$ .

givenchoose

1.2

Let $\ell'$ be an arbitrary lower bound of $S$ ; then $-\ell'$ is an upper bound of $-S$ .

assume-hypL2

2.1

Since $S$ is nonempty, so is $-S$ , and since $\ell_0$ is a lower bound of $S$ , its negative $-\ell_0$ is an upper bound of $-S$ ; hence $-S$ is a nonempty subset of $\mathbb{R}$ that is bounded above.

step 1.1L2

3.1

By the least-upper-bound property, $-S$ has a least upper bound in $\mathbb{R}$ ; write $u := \sup(-S)$ , which is well defined by uniqueness.

step 2.1L1L4

4.1

Define $\ell := -u$ .

step 3.1construct

4.2

The element $u$ is the least of the upper bounds of $-S$ and $-\ell'$ is one of them, hence $u \le -\ell'$ .

step 1.2step 3.1L1

5.1

Apply the reflection fact to the set $-S$ : since $u$ is an upper bound of $-S$ , its negative $-u$ is a lower bound of $-(-S)$ , and $-(-S) = S$ ; so $\ell = -u$ is a lower bound of $S$ .

step 4.1step 3.1L2

5.2

Negating the inequality $u \le -\ell'$ reverses it, giving $-(-\ell') \le -u$ , that is $\ell' \le \ell$ .

step 4.2step 4.1L5

6.1

Thus $\ell$ is a lower bound of $S$ satisfying $\ell' \le \ell$ for every lower bound $\ell'$ of $S$ , so $\ell$ is a greatest lower bound of $S$ ; it is the only one, so $\inf S$ exists and $\inf S = \ell = -\sup(-S)$ .

step 5.1step 5.2L3L4∎

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 $x \mapsto -x$ of Reflection through zero exchanges upper and lower bounds. Nothing about $\mathbb{R}$ 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 $\mathbb{R}$ has a supremum.
The identity $\inf S = -\sup(-S)$ 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

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 9 results over 6 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)
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)