Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck 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⊆R be nonempty and bounded below. Then S has a greatest lower bound in R (Greatest lower bound (infimum)), and it is given by

inf⁡S=−sup⁡(−S),where −S={−s:s∈S}.

In particular the complete ordered field 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⊆R that is bounded below, and its reflection −S={−s:s∈S}.

[L1]

The least-upper-bound property of R: every nonempty subset of R that is bounded above has a least upper bound in R, namely an upper bound that is ≤ 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 ℓ is a lower bound of X exactly when −ℓ is an upper bound of −X (Reflection through zero exchanges upper and lower bounds).

[L3]

Greatest lower bound (infimum): ℓ is one for S when ℓ is a lower bound of S and ℓ′≤ℓ for every lower bound ℓ′ 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≤b if and only if −b≤−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≠∅ and S is bounded below; fix a lower bound ℓ0 of S, so ℓ0≤s for every s∈S.

givenchoose
1.2

Let ℓ′ be an arbitrary lower bound of S; then −ℓ′ is an upper bound of −S.

assume-hypL2
2.1

Since S is nonempty, so is −S, and since ℓ0 is a lower bound of S, its negative −ℓ0 is an upper bound of −S; hence −S is a nonempty subset of R that is bounded above.

step 1.1L2
3.1

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

step 2.1L1L4
4.1

Define ℓ:=−u.

step 3.1construct
4.2

The element u is the least of the upper bounds of −S and −ℓ′ is one of them, hence u≤−ℓ′.

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 ℓ=−u is a lower bound of S.

step 4.1step 3.1L2
5.2

Negating the inequality u≤−ℓ′ reverses it, giving −(−ℓ′)≤−u, that is ℓ′≤ℓ.

step 4.2step 4.1L5
6.1

Thus ℓ is a lower bound of S satisfying ℓ′≤ℓ for every lower bound ℓ′ of S, so ℓ is a greatest lower bound of S; it is the only one, so inf⁡S exists and inf⁡S=ℓ=−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↦−x of Reflection through zero exchanges upper and lower bounds. Nothing about 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 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

…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