Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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.

Epsilon characterisation of the supremum

Statement

Let S⊆R be nonempty and bounded above, and let u be an upper bound of S (Complete ordered field (least-upper-bound property)). Then

u=sup⁡S⟺for every ε>0 there exists s∈S with u−ε<s.

In words: among the upper bounds of S, the supremum is exactly the one that cannot be lowered by any positive amount and still bound S.

Facts & Assumptions

Given: A nonempty S⊆R that is bounded above, and an upper bound u of S; since S is nonempty and bounded above, sup⁡S exists.

[L1]

Supremum: u=sup⁡S exactly when u is an upper bound of S and u≤u′ for every upper bound u′ of S; and every nonempty subset of R that is bounded above has such a least upper bound (Complete ordered field (least-upper-bound property)).

[L2]

The least upper bound is unique, so the equation u=sup⁡S says precisely that u is a least upper bound of S (Suprema and infima are unique).

[L3]

The order is total: for a,b∈R exactly one of a<b, a=b, b<a holds, so the negation of a≤b is b<a; and a<b holds exactly when b−a>0 (Complete ordered field (least-upper-bound property), Ordered field). (Translation invariance follows in one line from that last equivalence, since (b+c)−(a+c)=b−a, but no step below uses it and it is not claimed here as a quoted result.)

Proof

technique · direct
1.1

For the forward implication assume u=sup⁡S, that is, u is an upper bound of S that is ≤ every upper bound of S, and let ε>0 be arbitrary.

assume-hypL1L2
1.2

For the converse implication assume that u is an upper bound of S such that for every ε>0 there exists s∈S with u−ε<s, and let u′ be an arbitrary upper bound of S.

assume-hyp
2.1

Since u−(u−ε)=ε>0, we have u−ε<u.

step 1.1L3algebra
2.2

By totality either u≤u′ or u′<u; in the second case put ε0:=u−u′, so that ε0>0 and u−ε0=u′.

step 1.2L3algebra
3.1

The element u−ε is not an upper bound of S: if it were, the leastness of u among upper bounds would give u≤u−ε, which contradicts u−ε<u by trichotomy.

step 2.1step 1.1L1L3
3.2

In that second case the hypothesis applied to ε0 yields s0∈S with u′=u−ε0<s0, so s0≤u′ fails, contradicting that u′ is an upper bound of S; the second case is therefore impossible and u≤u′.

step 2.2step 1.2L3
4.1

Failing to be an upper bound of S means precisely that some s∈S does not satisfy s≤u−ε, and by totality that says u−ε<s; since ε>0 was arbitrary, the forward implication is proved.

step 3.1L3
4.2

Since u′ was an arbitrary upper bound of S, we get u≤u′ for every upper bound u′; as u is itself an upper bound, u is a least upper bound of S, hence u=sup⁡S by uniqueness, which proves the converse implication.

step 3.2step 1.2L1L2
5.1

Both implications hold, so for an upper bound u of a nonempty set S bounded above, u=sup⁡S if and only if for every ε>0 there is s∈S with u−ε<s.

step 4.1step 4.2∎

Depends on

Used by

Dependency tree · two levels

5 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