LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (openai/gpt-5.4)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.

Suprema and infima are unique

Statement

Let $S \subseteq R$ . If $u_{1}$ and $u_{2}$ are both least upper bounds of $S$ (Complete ordered field (least-upper-bound property)), then $u_{1} = u_{2}$ . If $ℓ_{1}$ and $ℓ_{2}$ are both greatest lower bounds of $S$ (Greatest lower bound (infimum)), then $ℓ_{1} = ℓ_{2}$ .

Consequently a set has at most one supremum and at most one infimum, and the notations $\sup S$ and $\inf S$ denote single, well-determined real numbers whenever they exist.

Facts & Assumptions

Given: A subset $S \subseteq R$ of the complete ordered field $R$ , together with elements $u_{1}, u_{2}, ℓ_{1}, ℓ_{2} \in R$ .

[L1]

$u$ is a least upper bound of $S$ exactly when $u$ is an upper bound of $S$ and $u \leq u^{'}$ for every upper bound $u^{'}$ of $S$ (Complete ordered field (least-upper-bound property)).

[L2]

$ℓ$ is a greatest lower bound of $S$ exactly when $ℓ$ is a lower bound of $S$ and $ℓ^{'} \leq ℓ$ for every lower bound $ℓ^{'}$ of $S$ (Greatest lower bound (infimum)).

[L3]

Antisymmetry of the order: for $a, b \in R$ , if $a \leq b$ and $b \leq a$ then $a = b$ . This is trichotomy in the underlying ordered field, which says that exactly one of $a < b$ , $a = b$ , $b < a$ holds, so, reasoning by contradiction, $a \neq b$ would put both $a < b$ and $b < a$ in force, which trichotomy forbids (Complete ordered field (least-upper-bound property), Ordered field).

Proof

technique · direct

1.1assume-hypL1

Assume $u_{1}$ and $u_{2}$ are both least upper bounds of $S$ ; in particular each of them is an upper bound of $S$ and each is $\leq$ every upper bound of $S$ .

1.2assume-hypL2

Assume $ℓ_{1}$ and $ℓ_{2}$ are both greatest lower bounds of $S$ ; in particular each of them is a lower bound of $S$ and each is $\geq$ every lower bound of $S$ .

2.1step 1.1L1

Applying the leastness of $u_{1}$ to the upper bound $u_{2}$ gives $u_{1} \leq u_{2}$ , and applying the leastness of $u_{2}$ to the upper bound $u_{1}$ gives $u_{2} \leq u_{1}$ .

2.2step 1.2L2

Applying the greatestness of $ℓ_{1}$ to the lower bound $ℓ_{2}$ gives $ℓ_{2} \leq ℓ_{1}$ , and applying the greatestness of $ℓ_{2}$ to the lower bound $ℓ_{1}$ gives $ℓ_{1} \leq ℓ_{2}$ .

3.1step 2.1step 2.2L3∎

By antisymmetry $u_{1} = u_{2}$ and $ℓ_{1} = ℓ_{2}$ , so a least upper bound and a greatest lower bound of $S$ are each unique when they exist, which is what licenses writing $\sup S$ and $\inf S$ .

Suprema and infima are unique

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources