Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
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 subset of R‾ has a least upper bound and a greatest lower bound in R‾, agreeing with the real supremum and infimum on nonempty sets bounded in R

Statement

Let A⊆R‾ be any subset of the extended real line (The extended real line R‾=R∪{−∞,+∞}, its order, and the arithmetic that is left undefined) and write AR:=A∩R. Then A has a least upper bound and a greatest lower bound in R‾ (Upper bound, least upper bound, and strict upper bound), each unique, which we write sup⁡A and inf⁡A with the ambient set always R‾. Explicitly:

  • sup⁡A=+∞ if +∞∈A, or if AR is not bounded above in R;
  • sup⁡A=−∞ if +∞∉A and AR=∅;
  • sup⁡A is the real supremum sup⁡AR (Complete ordered field (least-upper-bound property)) if +∞∉A and AR is nonempty and bounded above in R;

and dually, with −∞ and +∞ exchanged and "above" replaced by "below", for inf⁡A (Greatest lower bound (infimum), Every nonempty set bounded below has an infimum).

Agreement. If A⊆R is nonempty and bounded above in R (Lower bound, bounded below, bounded set) then sup⁡A computed in R‾ is the real number sup⁡A of Complete ordered field (least-upper-bound property); if A⊆R is nonempty and bounded below then inf⁡A computed in R‾ is the real number inf⁡A of Every nonempty set bounded below has an infimum. In particular the notation is unambiguous on the sets for which the real supremum and infimum are defined, and sup⁡∅=−∞, inf⁡∅=+∞ in R‾.

No hypothesis is placed on A. This is exactly what the real supremum cannot do, and it is why every lim sup⁡ statement on this page holds for every sequence rather than for bounded ones only. It is also not a weakening of the discipline this library keeps around suprema: the operation supplied here is a different operation, taken in a different ordered set, and the agreement clause records exactly where the two coincide.

Facts & Assumptions

Given: A subset A⊆R‾, and its real part AR:=A∩R.

[L1]

(R‾,≤) is a totally ordered set in which −∞ is the least element and +∞ the greatest, and whose order restricted to R is the order of R (The extended real line R‾=R∪{−∞,+∞}, its order, and the arithmetic that is left undefined, Partial order and partially ordered set, Order on the reals).

[L2]

Upper and lower bounds in a poset: u is an upper bound of A when a≤u for all a∈A, and a least upper bound when moreover u≤v for every upper bound v; dually for lower bounds and greatest lower bounds. Each is unique when it exists, by antisymmetry (Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L3]

Least-upper-bound property of R: every nonempty S⊆R that is bounded above in R has a real least upper bound sup⁡S (Complete ordered field (least-upper-bound property)).

[L4]

Greatest-lower-bound property of R: every nonempty S⊆R that is bounded below in R has a real greatest lower bound inf⁡S (Every nonempty set bounded below has an infimum, Greatest lower bound (infimum)).

[L5]

Bounded above and bounded below in R mean the existence of a real upper, respectively lower, bound (Lower bound, bounded below, bounded set).

Proof

technique · cases
1.1

Case S1 for the supremum: +∞∈A.

givenassume-case suptop
1.2

Case S2 for the supremum: +∞∉A and AR=∅, so that every element of A equals −∞.

givenassume-case supbot
1.3

Case S3 for the supremum: +∞∉A, AR≠∅, and AR is bounded above in R.

givenassume-case supfin
1.4

Case S4 for the supremum: +∞∉A, AR≠∅, and AR is not bounded above in R.

givenassume-case supunb
1.5

Case I1 for the infimum: −∞∈A.

givenassume-case infbot
1.6

Case I2 for the infimum: −∞∉A and AR=∅, so that every element of A equals +∞.

givenassume-case inftop
1.7

Case I3 for the infimum: −∞∉A, AR≠∅, and AR is bounded below in R.

givenassume-case inffin
1.8

Case I4 for the infimum: −∞∉A, AR≠∅, and AR is not bounded below in R.

givenassume-case infunb
2.1

In case S1 the element +∞ is an upper bound of A, being the greatest element of R‾; and if v is any upper bound of A then +∞∈A gives +∞≤v, whence v=+∞ by antisymmetry. So +∞ is the least upper bound of A.

step 1.1L1L2
2.2

In case S2 every element of A equals −∞, so −∞ is an upper bound of A by reflexivity; and −∞≤v for every v∈R‾, being the least element. So −∞ is the least upper bound of A.

step 1.2L1L2
2.3

In case S3 the real number σ:=sup⁡AR exists, and it is an upper bound of A in R‾: an element of A is either real, hence lies in AR and satisfies a≤σ in R and so in R‾, or equals −∞, which is ≤σ; the value +∞ does not occur in A in this case.

step 1.3L1L3
2.4

In case S4 the element +∞ is an upper bound of A; and if v is an upper bound then v≠−∞, because fixing a∈AR, which is possible in this case, gives a≤v with a real and −∞ is below no real, while v real would make v a real upper bound of AR and contradict the case hypothesis. So v=+∞, and +∞ is the least upper bound of A.

step 1.4L1L2L5
2.5

In case I1 the element −∞ is a lower bound of A, being least; and any lower bound w satisfies w≤−∞ because −∞∈A, whence w=−∞ by antisymmetry. So −∞ is the greatest lower bound of A.

step 1.5L1L2
2.6

In case I2 every element of A equals +∞, so +∞ is a lower bound of A by reflexivity, and w≤+∞ for every w. So +∞ is the greatest lower bound of A.

step 1.6L1L2
2.7

In case I3 the real number ι:=inf⁡AR exists and is a lower bound of A in R‾: an element of A is either real, hence in AR and ≥ι, or equals +∞≥ι; the value −∞ does not occur in A in this case.

step 1.7L1L4
2.8

In case I4 the element −∞ is a lower bound of A; any lower bound w satisfies w≠+∞, because fixing a∈AR gives w≤a with a real and +∞ is above no real, while w real would be a real lower bound of AR and contradict the case hypothesis. So w=−∞ is the greatest lower bound of A.

step 1.8L1L2L5
3.1

In case S3 let v be any upper bound of A and fix a∈AR, which is possible since AR≠∅. From a≤v with a real we get v≠−∞, since −∞ is below no real. If v=+∞ then σ≤v because +∞ is greatest. Otherwise v is real, and it bounds AR above in R, so σ≤v by leastness of the real supremum. Hence σ is the least upper bound of A.

step 1.3step 2.3L1L2L3
3.2

In case I3 let w be a lower bound of A and fix a∈AR. From w≤a with a real we get w≠+∞. If w=−∞ then w≤ι; otherwise w is real and bounds AR below in R, so w≤ι. Hence ι is the greatest lower bound of A.

step 1.7step 2.7L1L2L4
4.1

The four supremum cases are exhaustive and mutually exclusive: either +∞∈A, which is S1, or not, and then either AR=∅, which is S2, or AR≠∅ and it is bounded above in R, which is S3, or it is not, which is S4. In each case a least upper bound was produced, and it is unique. The same four alternatives with −∞, +∞ and "below" in place of +∞, −∞ and "above" are I1 to I4, and in each a greatest lower bound was produced.

step 2.1step 2.2step 3.1step 2.4step 2.5step 2.6step 3.2step 2.8L2L5cases: a two-fold split followed by a three-fold splitcases-exhaustive
5.1

The agreement clause follows: a nonempty A⊆R bounded above in R satisfies +∞∉A and AR=A, so case S3 applies and sup⁡A=sup⁡AR is the real supremum; a nonempty A⊆R bounded below satisfies case I3 and inf⁡A is the real infimum; and A=∅ falls under S2 and I2, giving sup⁡∅=−∞ and inf⁡∅=+∞.

step 2.3step 3.1step 2.7step 3.2step 4.1L3L4∎

Remarks

Depends on

Used by

…and 11 more results.

Dependency tree · two levels

17 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