Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

On (0,1) the identity is bounded with no greatest value and x↦1/x is continuous and unbounded, so the extreme value theorem needs compactness and not merely boundedness of the domain

Statement refuted

Refuted claim: a continuous real-valued function on a nonempty bounded metric space is bounded and attains a greatest value.

The true statement replaces bounded by compact (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value), and the difference is not cosmetic. The witness is the interval (0,1) (Intervals of R: the nine order-convex forms, nondegeneracy, and length) as a metric subspace of R (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), which is bounded (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space) and not compact (The open interval (0,1) is totally bounded and not compact, the cover by the intervals (1/(k+2),1) having no finite subcover), together with two continuous functions on it (Continuity of a map between metric spaces, at a point and globally, in the ε-δ form):

  • the identity f(x)=x, which is bounded, has supremum 1, and attains no greatest value;
  • the map g(x)=1/x, which is continuous and unbounded.

So on a merely bounded domain a continuous function may fail to attain its supremum, and may fail to be bounded at all.

Facts & Assumptions

Given: The interval (0,1) with the metric ∣x−y∣ restricted to it, and the functions f(x)=x and g(x)=1/x on it.

[A1]

The refuted claim: a continuous real-valued function on a nonempty bounded metric space is bounded and attains a greatest value.

[L2]

h is continuous at c when for every real ε>0 there is a real δ>0 with ∣h(x)−h(c)∣<ε whenever ∣x−c∣<δ (Continuity of a map between metric spaces, at a point and globally, in the ε-δ form).

[L3]

u=sup⁡S for a nonempty S bounded above exactly when u is an upper bound and for every real ε>0 some s∈S has u−ε<s; a maximum is a member of the set that bounds it above (Epsilon characterisation of the supremum, Maximum and minimum of a set, Lower bound, bounded below, bounded set, Complete ordered field (least-upper-bound property)).

[L4]

For every real M there is a natural N≥1 with M<ι(N), for every real η>0 a natural N≥1 with 1/N<η, and reciprocals of positives are positive and reverse the order (Every complete ordered field is Archimedean, For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Inverses of positives are positive, and reciprocation reverses order).

[L5]

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

Counterexample

technique · direct
1.1

The identity f is continuous on (0,1), δ:=ε serving at every point, and its image is (0,1), which is bounded above by 1 and below by 0.

L1L2
2.1

sup⁡f[(0,1)]=1: the value 1 is an upper bound, and for a real ε>0 the point x:=max⁡{1−ε/2, 1/2} lies in (0,1) and satisfies x>1−ε.

L3step 1.1
3.1

f attains no greatest value: for x∈(0,1) the point (x+1)/2 lies in (0,1) and satisfies (x+1)/2>x, so no member of the image bounds the image above.

L3step 2.1
4.1

g(x)=1/x is defined on (0,1), every x there being positive, and it is continuous at each c∈(0,1): given a real ε>0, the choice δ:=min⁡{c/2, εc2/2} gives, for ∣x−c∣<δ, first x>c/2>0 and then ∣1/x−1/c∣=∣c−x∣/(xc)<(2/c2)∣x−c∣<ε.

L2L4step 3.1
5.1

g is unbounded on (0,1): given a real M, take a natural N≥1 with M<ι(N); the point x:=1/ι(N+1) lies in (0,1) and g(x)=ι(N+1)>ι(N)>M.

L4step 4.1
6.1

So on the nonempty bounded non-compact space (0,1) the continuous function f is bounded and attains no greatest value, and the continuous function g is not even bounded; the claim [A1] is refuted, and the compactness hypothesis of the extreme value theorem cannot be weakened to boundedness.

A1L1L5step 1.1step 3.1step 5.1∎

Remarks

Which hypothesis each failure isolates. The identity shows that the attainment half of A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value fails on a bounded non-compact domain even for a bounded function; the map 1/x shows that the boundedness half fails too. Compactness is what supplies both, through the image being closed and bounded (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, A compact subset of a metric space is closed and bounded).

Closing the interval repairs the first example and rules out the second. On [0,1], which is compact (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line), the identity attains the value 1. The map 1/x has no continuous extension to [0,1] at all: such an extension would be bounded by [L5], whereas its restriction to (0,1) is unbounded by step 5.1. So the failure of the second example is a failure of the domain, not of the theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 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