TheoremStatement: AI-adaptedProof: AI-generatedprecheck pass

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-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value

Statement

Let $(X, d)$ be a nonempty compact metric space (Open cover, subcover, compact metric space, and compact subset of a metric space, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) and let $f : X \to R$ be continuous (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form), $R$ carrying its usual metric $d_{R} (s, t) = ∣ s - t ∣$ (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded). Then the image $f [X]$ is bounded above and below (Lower bound, bounded below, bounded set), and it has a maximum and a minimum (Maximum and minimum of a set): there are points $x_{\max}, x_{\min} \in X$ with

$f (x_{\min}) \leq f (x) \leq f (x_{\max}) for every x \in X,$

and then $f (x_{\max}) = \sup f [X]$ and $f (x_{\min}) = \inf f [X]$ (Complete ordered field (least-upper-bound property), Greatest lower bound (infimum)).

Nonemptiness of $X$ is a hypothesis and not an oversight: for $X = \emptyset$ the image is empty and has neither a supremum nor a maximum. No choice principle is used.

Statement references

Open cover, subcover, compact metric space, and compact subset of a metric space

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric

Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form

The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded

Lower bound, bounded below, bounded set

Maximum and minimum of a set

Complete ordered field (least-upper-bound property)

Greatest lower bound (infimum)

Facts & Assumptions

Given: A nonempty compact metric space $(X, d)$ and a continuous $f : X \to R$ .

[L1]

The image of a compact metric space under a continuous map is a compact subset of the codomain (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L2]

A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded, A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L3]

In $(R, d_{R})$ the ball $B (x_{0}, ρ)$ is the interval $(x_{0} - ρ, x_{0} + ρ)$ (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Open ball, closed ball and sphere in a metric space, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

A nonempty subset of $R$ that is bounded above has a supremum, and one bounded below has an infimum (Complete ordered field (least-upper-bound property), Every nonempty set bounded below has an infimum, Greatest lower bound (infimum), Lower bound, bounded below, bounded set).

[L5]

For $S$ nonempty and bounded above with supremum $u$ : for every real $ε > 0$ there is $s \in S$ with $u - ε < s \leq u$ ; dually for the infimum (Epsilon characterisation of the supremum, Epsilon characterisation of the infimum).

[L6]

$x$ lies in the closure of $S$ exactly when every ball around $x$ meets $S$ , and a closed set contains its closure (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[L7]

A subset of a metric space is compact exactly when the corresponding metric subspace is compact, the subspace metric being the restriction (Open cover, subcover, compact metric space, and compact subset of a metric space, Isometry, isometric embedding, and the subspace metric on a subset).

Proof

technique · direct

1.1L1L7

$f [X]$ is a compact subset of $(R, d_{R})$ , and it is nonempty because $X$ is.

2.1L2L3step 1.1

So $f [X]$ is closed in $R$ and bounded as a subset of the metric space $(R, d_{R})$ : there are $x_{0} \in R$ and a real $ρ > 0$ with $f [X] \subseteq B (x_{0}, ρ) = (x_{0} - ρ, x_{0} + ρ)$ .

3.1L4step 2.1

Hence $x_{0} + ρ$ is an upper bound and $x_{0} - ρ$ a lower bound of $f [X]$ , so $f [X]$ is bounded above and below, and being nonempty it has a supremum $u$ and an infimum $ℓ$ .

4.1L3L5L6step 3.1

For every real $ε > 0$ there is $t \in f [X]$ with $u - ε < t \leq u$ , so $∣ t - u ∣ < ε$ and $t \in B (u, ε) \cap f [X]$ ; therefore every ball around $u$ meets $f [X]$ and $u$ lies in the closure of $f [X]$ .

5.1L6step 2.1step 4.1

Since $f [X]$ is closed, $u \in f [X]$ ; so $u$ is a member of $f [X]$ bounding it above, that is $u = \max f [X]$ , and $u = f (x_{\max})$ for some $x_{\max} \in X$ .

6.1L5L6step 3.1step 5.1

The same argument with $ℓ$ in place of $u$ , using the infimum form of step 4.1, gives $ℓ \in f [X]$ , so $ℓ = \min f [X]$ and $ℓ = f (x_{\min})$ for some $x_{\min} \in X$ .

7.1L4step 3.1step 5.1step 6.1∎

For every $x \in X$ the value $f (x)$ lies in $f [X]$ , hence $f (x_{\min}) = ℓ \leq f (x) \leq u = f (x_{\max})$ , which is the assertion, with $f (x_{\max}) = \sup f [X]$ and $f (x_{\min}) = \inf f [X]$ .

Remarks

Compactness is what is used, not boundedness of the domain. A bounded non-compact domain is not enough: on the interval $(0, 1)$ the identity map is continuous and bounded with no greatest value, and $x \mapsto 1 / x$ is continuous and unbounded (On $(0, 1)$ the identity is bounded with no greatest value and $x \mapsto 1 / x$ is continuous and unbounded, so the extreme value theorem needs compactness and not merely boundedness of the domain ↗).

Why the supremum has to be shown to be attained at all. $\sup f [X]$ exists as soon as $f [X]$ is nonempty and bounded above, which needs only boundedness; what compactness adds is that $f [X]$ is closed, and a closed set contains the supremum it approaches. Steps 4.1 and 5.1 are exactly that passage, and they are where the theorem is more than the least-upper-bound property.

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value

Statement

Statement references

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources