Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-05
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.

Riesz's rising sun lemma with the correct endpoint conclusion

Statement

Let F:[a,b]→R be continuous (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) and put

E:={x∈[a,b):there is y∈(x,b] with F(y)>F(x)}.

Then E is an open subset of the subspace [a,b). Equivalently, E∩(a,b) is open in R, and every component of E is either an initial half-open interval [a,d) when a∈E, or an open interval (c,d) with a≤c<d≤b (Every open subset of R is a countable disjoint union of open intervals, namely its order components). For every component I of E with left endpoint c and right endpoint d one has

F(c)≤F(d),

and if c>a then in fact

F(c)=F(d).

Equivalently, every x∈I satisfies F(x)<F(d), while if c>a then F(x)<F(c)=F(d) for all x∈I.

Facts & Assumptions

Given: The continuous function F:[a,b]→R and the set E⊆[a,b) just defined.

[A1]

The symbols are those of the statement.

Proof

technique · direct
1.1

Let x∈E. Choose y>x with F(y)>F(x). By continuity at x, after shrinking if necessary there is ε with 0<ε<y−x such that F(t)<F(y) whenever ∣t−x∣<ε and t∈[a,b]. Every t∈(x−ε,x+ε)∩[a,b) then satisfies t<y and F(t)<F(y), so it also belongs to E. Thus E is open in the subspace [a,b). Therefore E∩(a,b) is open in R, and Every open subset of R is a countable disjoint union of open intervals, namely its order components writes it as a countable disjoint union of open intervals. A component meeting the left endpoint is [a,d) when a∈E; if a∉E, an open component may instead have the form (a,d). Thus every component of E is either [a,d) when a∈E, or (c,d) with a≤c<d≤b.

given
2.1

Fix a component I of E, write its left endpoint as c and its right endpoint as d, and let x∈I. By the extreme value theorem Extreme value theorem: a continuous real function on a nonempty compact subset of R attains a greatest and a least value, choose t∈[x,b] at which F attains its maximum on [x,b]. Since x∈E, some point to the right of x has value greater than F(x), so t>x and F(t)>F(x). The maximizing point t does not belong to E. Since every point of I lies in E, this forces t≥d. If d<b and F(t)>F(d), then necessarily t>d, which would put d in E, contrary to d being the right endpoint of the component. Thus F(t)≤F(d); the reverse inequality holds because d∈[x,b] and t is a maximizer. When d=b one has t=d directly. Hence in all cases F(x)<F(t)=F(d).

step 1.1
3.1

Letting x↓c through points of I in step 2.1 and using continuity at c gives F(c)≤F(d). If c>a, then c∉E, so no point to the right of c has value strictly larger than F(c); in particular F(d)≤F(c). Hence F(c)=F(d) when c>a.

step 2.1
4.1

Steps 1.1 through 3.1 are exactly the claimed conclusions.

step 1.1step 2.1step 3.1∎

Depends on

Used by

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