LemmaStatement: AI-adaptedProof: AI-adaptedSession-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.

Supremum of a sumset: $\sup(S + T) = \sup S + \sup T$

Statement

Let $S, T \subseteq \mathbb{R}$ be nonempty and bounded above, and write $S + T := \{s + t : s \in S,\ t \in T\}$ . Then $S + T$ is nonempty and bounded above, and

$\sup(S + T) = \sup S + \sup T.$

Facts & Assumptions

Given: Nonempty sets $S, T \subseteq \mathbb{R}$ , both bounded above, and the sumset $S + T = \{s + t : s \in S,\ t \in T\}$ .

[L1]

Epsilon characterisation of the supremum: for a nonempty $X \subseteq \mathbb{R}$ bounded above and an upper bound $w$ of $X$ , one has $w = \sup X$ if and only if for every $\varepsilon > 0$ there is $x \in X$ with $w - \varepsilon < x$ (Epsilon characterisation of the supremum).

[L2]

Order and addition: strict inequalities translate and add, that is $x < y$ implies $x + c < y + c$ , and $x < y$ together with $z < w$ gives $x + z < y + w$ (claims 1 and 2 of Order is preserved by adding a constant and by adding inequalities). Adjoining the case of equality, in which both sides move by the same amount, gives the nonstrict forms used below: $x \le y$ implies $x + c \le y + c$ , and $x \le y$ together with $z \le w$ gives $x + z \le y + w$ .

[L3]

Supremum and the least-upper-bound property: $w = \sup X$ means $w$ is an upper bound of $X$ with $w \le w'$ for every upper bound $w'$ of $X$ , and every nonempty $X \subseteq \mathbb{R}$ bounded above has such a $w$ (Complete ordered field (least-upper-bound property)).

[L4]

Halving: $0 < 1$ (The multiplicative identity is positive); the positives are closed under addition, so $2 := 1 + 1 > 0$ , and by trichotomy a positive element is nonzero, so $2 \ne 0$ (axioms O2 and O1 of Ordered field); hence $2^{-1}$ exists (Field) and $0 \cdot 2 = 0$ (Multiplication by zero: $0 \cdot a = 0$ ); and for the positive multiplier $2$ one has $x < y$ if and only if $x \cdot 2 < y \cdot 2$ (claim 4 of Sign rules for products and monotonicity of multiplication).

Proof

technique · direct

1.1

Both $S$ and $T$ are nonempty and bounded above, so the least-upper-bound property supplies $u := \sup S$ and $v := \sup T$ , upper bounds of $S$ and of $T$ respectively.

givenL3

1.2

The sumset $S + T$ is nonempty: picking $s \in S$ and $t \in T$ , which is possible since both sets are nonempty, gives $s + t \in S + T$ .

given

2.1

For $s \in S$ and $t \in T$ we have $s \le u$ and $t \le v$ , and adding these inequalities gives $s + t \le u + v$ ; since every element of $S + T$ has this form, $u + v$ is an upper bound of $S + T$ , so $S + T$ is bounded above.

step 1.1L2

2.2

Let $\varepsilon > 0$ and put $\eta := \varepsilon \cdot 2^{-1}$ , so that $\eta \cdot 2 = \varepsilon$ and $\eta + \eta = \eta(1 + 1) = \varepsilon$ ; from $0 \cdot 2 = 0 < \varepsilon = \eta \cdot 2$ and $2 > 0$ we get $\eta > 0$ , so the epsilon characterisation applied to $S$ with $u$ and to $T$ with $v$ produces $s \in S$ with $u - \eta < s$ and $t \in T$ with $v - \eta < t$ , and adding these strict inequalities gives $(u + v) - \varepsilon = (u - \eta) + (v - \eta) < s + t$ , an element of $S + T$ .

step 1.1L1L2L4algebra

3.1

The set $S + T$ is nonempty and bounded above, so $\sup(S + T)$ exists.

step 1.2step 2.1L3

4.1

Now $u + v$ is an upper bound of $S + T$ and for every $\varepsilon > 0$ some element of $S + T$ exceeds $(u + v) - \varepsilon$ , so the epsilon characterisation applied to $S + T$ gives $\sup(S + T) = u + v = \sup S + \sup T$ .

step 2.1step 2.2step 3.1L1∎

Remarks

The inequality $\sup(S + T) \le \sup S + \sup T$ is the easy half and needs only that $u + v$ bounds $S + T$ ; the content is the reverse inequality, and the halving of $\varepsilon$ is what lets two separate approximations be combined without overshooting.
The corresponding statement for infima, $\inf(S + T) = \inf S + \inf T$ for nonempty $S, T$ bounded below, follows by reflection (Reflection through zero exchanges upper and lower bounds, Every nonempty set bounded below has an infimum), since $-(S + T) = (-S) + (-T)$ .
No analogue holds for products in general: sign changes break the argument, and $\sup(ST)$ is not determined by $\sup S$ and $\sup T$ alone.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 12 results over 5 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)
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)
Peter J. Olver, Continuous Calculus (standard reference, not scraped)

Supremum of a sumset: sup⁡(S+T)=sup⁡S+sup⁡T\sup(S + T) = \sup S + \sup Tsup(S+T)=supS+supT