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.
A continuous real function on a compact subset of is bounded
Statement
Let , let be continuous on (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point) and let be compact (Open cover, subcover, compact subset of (every open cover has a finite subcover), and sequentially compact subset). Then is bounded on : there is a real with
Equivalently, is a bounded subset of (Lower bound, bounded below, bounded set).
The hypothesis is compactness of , not of , and it cannot be relaxed to boundedness of or to closedness of alone: the identity is unbounded on the closed set , and is unbounded on the bounded set . The general statement of that is Rudin 4.20, the sharp converse: on a noncompact there is an unbounded continuous function and a bounded continuous function with no greatest value, and if is bounded there is a continuous function on that is not uniformly continuous, later on this page.
Facts & Assumptions
Given: A set , a function continuous on , and a compact set .
The image is compact (The image of a compact subset of under a continuous real function is compact, Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point, Open cover, subcover, compact subset of (every open cover has a finite subcover), and sequentially compact subset).
A subset of is compact if and only if it is closed and bounded (A subset of is compact if and only if it is closed and bounded).
A set is bounded when there are reals with for every (Lower bound, bounded below, bounded set).
A nonempty finite set of reals has a maximum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set), and the order of is total (Ordered field).
Absolute value: ; when and when ; and for every real (Basic properties of the absolute value).
Proof
By [L1] the set is compact, and by [L2] it is therefore closed and bounded.
By [L3] fix reals and with for every , and put , which exists by [L4] and satisfies by [L5].
Let and put , so . If then ; if then , using and . In both cases .
So for every , with a real; equivalently is bounded, which is what step 1.1 already recorded.
Remarks
-
Boundedness is the weak half of the extreme value theorem. What compactness gives in addition is that the two bounds are attained, which is Extreme value theorem: a continuous real function on a nonempty compact subset of attains a greatest and a least value; the supremum of exists as soon as is nonempty and bounded above, and the work is entirely in showing that it belongs to .
-
Boundedness of the domain is not what is used. The proof never looks at after the first line: the whole content is that the image is compact, hence bounded. That is why the same one-line argument gives boundedness of a continuous function on any compact set, however complicated.
Depends on
The image of a compact subset of under a continuous real function is compact
A subset of is compact if and only if it is closed and bounded
Open cover, subcover, compact subset of (every open cover has a finite subcover), and sequentially compact subset
Lower bound, bounded below, bounded set
Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point
Maximum and minimum of a set
Every nonempty finite set of reals has a maximum and a minimum
Basic properties of the absolute value
Ordered field