TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-09 (gpt-5.6-terra-codex-subscription)

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.

Semicontinuous extreme value theorem: an upper semicontinuous function on a nonempty compact $K \subseteq R$ is bounded above and attains a maximum, and a lower semicontinuous one is bounded below and attains a minimum

Statement

Let $K \subseteq R$ be nonempty and compact (Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset).

If $f : K \to R$ is upper semicontinuous on $K$ (Upper and lower semicontinuity of $f : A \to R$ at a point of $A$ and on $A$ ) then $f [K]$ is bounded above (Lower bound, bounded below, bounded set) and $f$ attains a maximum: there is $x_{0} \in K$ with $f (x) \leq f (x_{0})$ for every $x \in K$ (Maximum and minimum of a set).
If $f : K \to R$ is lower semicontinuous on $K$ then $f [K]$ is bounded below and $f$ attains a minimum.

The theorem is genuinely one-sided. An upper semicontinuous function on a compact set need not attain its infimum; the companion page gives such a function on $[0, 1]$ . Only the maximum is asserted in claim 1, and only the minimum in claim 2.

Taking $f$ continuous, which is upper and lower semicontinuous at once (Upper and lower semicontinuity of $f : A \to R$ at a point of $A$ and on $A$ ), recovers the classical extreme value theorem on a compact subset of $R$ .

Facts & Assumptions

Given: A nonempty compact $K \subseteq R$ and an upper semicontinuous $f : K \to R$ .

[L1]

For every real $α$ there is an open $U_{α} \subseteq R$ with $U_{α} \cap K = {x \in K : f (x) < α}$ , namely $U_{α} = {y \in R : K \cap N_{ρ} (y) \subseteq {f < α}$ for some real $ρ > 0}$ ( $f$ is upper semicontinuous on $A$ if and only if ${x \in A : f (x) < α}$ is relatively open in $A$ for every real $α$ , lower semicontinuous if and only if ${x \in A : f (x) > α}$ is, and continuous if and only if it is both, Upper and lower semicontinuity of $f : A \to R$ at a point of $A$ and on $A$ , Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen).

[L2]

The set $U_{α}$ of [L1] is monotone in $α$ : $α \leq β$ gives ${f < α} \subseteq {f < β}$ and hence $U_{α} \subseteq U_{β}$ , directly from the displayed description.

[L3]

$K$ compact means: every family of open subsets of $R$ whose union contains $K$ has a finite subfamily whose union contains $K$ (Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset).

[L4]

For every real $x$ there is a natural $n \geq 1$ with $x < ι (n)$ , and for every real $η > 0$ a natural $n \geq 1$ with $1 / ι (n) < η$ ; $ι$ is positive and strictly increasing on the naturals $\geq 1$ (Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L5]

A nonempty set of reals bounded above has a least upper bound, and for every real $ε > 0$ some member of the set exceeds $\sup - ε$ (Complete ordered field (least-upper-bound property), Epsilon characterisation of the supremum, Lower bound, bounded below, bounded set).

[L6]

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).

[L7]

For any $h : K \to R$ , $h$ is upper semicontinuous if and only if $- h$ is lower semicontinuous; hence a lower semicontinuous $f$ makes $- f$ upper semicontinuous (Upper and lower semicontinuity of $f : A \to R$ at a point of $A$ and on $A$ , section “Negation exchanges the two”).

Proof

technique · direct

1.1

For each real $α$ let $U_{α}$ be the open set of [L1], so that $U_{α} \cap K = {x \in K : f (x) < α}$ and $α \leq β$ implies $U_{α} \subseteq U_{β}$ .

L1L2construct

2.1

The family ${U_{ι (n)} : n \in N, n \geq 1}$ covers $K$ : every $x \in K$ has $f (x) < ι (n)$ for some natural $n \geq 1$ , and then $x \in U_{ι (n)}$ .

step 1.1L4

3.1

By compactness finitely many members cover $K$ , say $U_{ι (n_{0})}, \dots, U_{ι (n_{j})}$ with each $n_{i} \geq 1$ ; let $N$ be the greatest of $ι (n_{0}), \dots, ι (n_{j})$ , which exists as the maximum of a nonempty finite set of reals. Then each $U_{ι (n_{i})} \subseteq U_{N}$ , so $K \subseteq U_{N}$ and hence $K = U_{N} \cap K = {x \in K : f (x) < N}$ . So $f [K]$ is bounded above by $N$ .

step 1.1step 2.1L2L3L6

4.1

$f [K]$ is nonempty, since $K$ is, and bounded above, so $M : = \sup f [K]$ exists.

step 3.1L5

5.1

For each natural $n \geq 1$ put $α_{n} : = M - 1 / ι (n)$ . The family ${U_{α_{n}} : n \geq 1}$ has no finite subfamily covering $K$ . Indeed, let $U_{α_{n_{0}}}, \dots, U_{α_{n_{j}}}$ be finitely many of them; if the list is empty its union is empty and does not contain the nonempty $K$ . Otherwise let $n^{*}$ be a natural among $n_{0}, \dots, n_{j}$ with $α_{n^{*}}$ greatest, so that every member of the list is contained in $U_{α_{n^{*}}}$ . Since $α_{n^{*}} < M = \sup f [K]$ , there is $x \in K$ with $f (x) > α_{n^{*}}$ , and such an $x$ lies in $K$ but not in $U_{α_{n^{*}}} \cap K = {f < α_{n^{*}}}$ , hence in no member of the list.

step 1.1step 4.1L2L4L5L6

6.1

By compactness, a family of open sets with no finite subfamily covering $K$ cannot itself cover $K$ . So there is $x_{0} \in K$ with $x_{0} \notin U_{α_{n}}$ for every natural $n \geq 1$ , that is $f (x_{0}) \geq α_{n} = M - 1 / ι (n)$ for every such $n$ .

step 1.1step 5.1L3

7.1

Hence $f (x_{0}) = M$ . If $f (x_{0}) < M$ then $M - f (x_{0}) > 0$ and there is a natural $n \geq 1$ with $1 / ι (n) < M - f (x_{0})$ , that is $f (x_{0}) < M - 1 / ι (n)$ , contradicting step 6.1; and $f (x_{0}) \leq M$ because $M$ is an upper bound of $f [K]$ .

step 4.1step 6.1L4L5

8.1

So $f$ is bounded above on $K$ and attains the value $M = \sup f [K]$ at $x_{0} \in K$ , which is a maximum of $f [K]$ : this is claim 1.

step 3.1step 4.1step 7.1L5

9.1

Claim 2 follows by applying claim 1 to $- f$ , which is upper semicontinuous on $K$ when $f$ is lower semicontinuous; then $- f$ is bounded above and attains a maximum at some $x_{1} \in K$ , so $f$ is bounded below and $f (x_{1}) \leq f (x)$ for every $x \in K$ , a minimum.

step 8.1L7∎

Remarks

Where compactness is spent, and in which form. Twice, and both times as the open-cover property of Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset: once to bound $f$ above, once to find the point where the supremum is attained. No sequence is extracted and no countable choice is used; the second application is stated as the contrapositive of the covering property, which is why step 5.1 proves that no finite subfamily covers rather than assuming a limit point.
Semicontinuity cannot be dropped. Both applications use only that the sets ${f < α}$ are relatively open ( $f$ is upper semicontinuous on $A$ if and only if ${x \in A : f (x) < α}$ is relatively open in $A$ for every real $α$ , lower semicontinuous if and only if ${x \in A : f (x) > α}$ is, and continuous if and only if it is both), which is exactly upper semicontinuity, and nothing else about $f$ is used at all. A function whose strict sublevel sets are not relatively open can be unbounded above on a compact set: the function on $[0, 1]$ equal to $1 / x$ for $x \neq 0$ and to $0$ at $0$ is one.

Depends on

Used by

An upper semicontinuous function on [0,1] that is bounded below and attains no minimum, so the semicontinuous extreme value theorem is genuinely one-sided Counterexample

Dependency tree · two levels

31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Semi-continuity (Wikipedia) (standard reference, not scraped)
Extreme value theorem (Wikipedia) (standard reference, not scraped)
Upper Semicontinuous Function on Compact Space Attains Maximum (ProofWiki) (standard reference, not scraped)

Semicontinuous extreme value theorem: an upper semicontinuous function on a nonempty compact K⊆RK⊆R is bounded above and attains a maximum, and a lower semicontinuous one is bounded below and attains a minimum