LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Monotonicity of the supremum under inclusion

Statement

Let $S$ and $T$ be subsets of $\mathbb{R}$ with $\emptyset \ne S \subseteq T$ , and suppose $T$ is bounded above. Then $S$ is nonempty and bounded above, both $\sup S$ and $\sup T$ exist, and

$\sup S \le \sup T.$

Facts & Assumptions

Given: Sets $S, T \subseteq \mathbb{R}$ with $S \ne \emptyset$ , $S \subseteq T$ , and $T$ bounded above.

[L1]

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

[L2]

A least upper bound is unique, so $\sup X$ denotes a single real number (Suprema and infima are unique).

Proof

technique · direct

1.1

Since $T$ is bounded above, fix an upper bound $u$ of $T$ , so $t \le u$ for every $t \in T$ .

givenchoose

1.2

By hypothesis $S$ is nonempty and $S \subseteq T$ , so $T$ is nonempty as well.

given

2.1

Every $s \in S$ lies in $T$ and therefore satisfies $s \le u$ ; hence $u$ is an upper bound of $S$ and $S$ is bounded above.

step 1.1step 1.2L1

3.1

Both $S$ and $T$ are nonempty and bounded above, so by the least-upper-bound property $\sup S$ and $\sup T$ exist, each uniquely.

step 1.2step 2.1L1L2

4.1

As $\sup T$ is an upper bound of $T$ , every $t \in T$ satisfies $t \le \sup T$ ; since $S \subseteq T$ , every $s \in S$ satisfies $s \le \sup T$ , so $\sup T$ is an upper bound of $S$ .

step 3.1step 1.2L1

5.1

The number $\sup S$ is the least of the upper bounds of $S$ , and $\sup T$ is one of them, hence $\sup S \le \sup T$ .

step 4.1step 3.1L1∎

Remarks

The hypothesis that the larger set is bounded above cannot be weakened to the smaller one being bounded above: $\sup T$ has to exist for the inequality to mean anything.
The dual statement, $\inf T \le \inf S$ for $\emptyset \ne S \subseteq T$ with $T$ bounded below, follows by applying this lemma to $\emptyset \ne -S \subseteq -T$ , which gives $\sup(-S) \le \sup(-T)$ , and then negating and using $\inf X = -\sup(-X)$ (Reflection through zero exchanges upper and lower bounds, Every nonempty set bounded below has an infimum).

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 6 results over 6 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)