Alphabeta Math
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 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.

FALSE: a continuous real function on a bounded domain attains a greatest value

Statement

False claim: if E⊆R is nonempty and bounded (Lower bound, bounded below, bounded set) and f:E→R is continuous on E (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point), then f attains a greatest value on E: there is p∈E with f(x)≤f(p) for every x∈E (Maximum and minimum of a set).

Why it is tempting. The extreme value theorem is often remembered as "a continuous function on a bounded interval attains its bounds", and on [a,b] that is true. The hypothesis that actually does the work is compactness, which for a subset of R is closed and bounded (A subset of R is compact if and only if it is closed and bounded); dropping closedness loses the theorem even though the function may stay bounded.

What is true. Extreme value theorem: a continuous real function on a nonempty compact subset of R attains a greatest and a least value gives the conclusion on a nonempty compact domain, and the hypothesis cannot be weakened: for every noncompact E there is a bounded continuous function on E whose supremum is not attained, which is Rudin 4.20, the sharp converse: on a noncompact E⊆R there is an unbounded continuous function and a bounded continuous function with no greatest value, and if E is bounded there is a continuous function on E that is not uniformly continuous. The witness below is that theorem's simplest instance.

Facts & Assumptions

Given: The domain E:=(0,1)={ x∈R:0<x<1 } (Intervals of R: the nine order-convex forms, nondegeneracy, and length) and the function f:E→R, f(x):=x.

[L1]

E is nonempty and bounded: 1/2∈E, and 0≤x≤1 for every x∈E (Lower bound, bounded below, bounded set, Intervals of R: the nine order-convex forms, nondegeneracy, and length, Ordered field).

[L3]

A greatest value of f on E is a point p∈E with f(x)≤f(p) for every x∈E; equivalently a maximum of f[E] lying in f[E] (Maximum and minimum of a set).

[L4]

Ordered-field arithmetic in R: for 0<x<1 one has x<(x+1)/2<1; and 0<1 (Ordered field).

[L5]

Suprema: a nonempty set bounded above has a least upper bound, and for u=sup⁡S every real ε>0 admits s∈S with u−ε<s (Complete ordered field (least-upper-bound property), Epsilon characterisation of the supremum).

Refutation

technique · direct
1.1

E is nonempty and bounded by [L1], and f is continuous on E by [L2], so the hypotheses of the claim are satisfied.

L1L2
2.1

Let p∈E be arbitrary, so 0<p<1. Put p′:=(p+1)/2; by [L4] we have p<p′<1 and 0<p′, so p′∈E and f(p′)=p′>p=f(p). Hence no p∈E satisfies f(x)≤f(p) for every x∈E, and by [L3] the function f attains no greatest value on E.

step 1.1L3L4
3.1

The claim is therefore false. Note also what the failure is not: f[E]=E is nonempty and bounded above by 1, so sup⁡f[E] exists by [L5] and equals 1, since 1 bounds f[E] and for every real ε>0 the point x:=max⁡{1/2, 1−ε/2} lies in E with x>1−ε. What fails is only that 1∉f[E].

step 2.1L1L4L5∎

Remarks

Depends on

Used by

Dependency tree · two levels

43 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