Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-07-31
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.

Dini's theorem fails for a discontinuous limit: powers on [0,1] decrease pointwise to a discontinuous endpoint indicator but not uniformly

Statement refuted

Refuted claim: continuity of the pointwise limit in Dini's theorem can be dropped.

On [0,1] let fk(x)=xk+1. These continuous functions decrease pointwise to the discontinuous endpoint indicator

χ(x)={0,0≤x<1,1,x=1,

and the convergence is not uniform.

Facts & Assumptions

Given: The functions fk(x)=xk+1 and the endpoint indicator χ on [0,1].

[L1]

The powers xk+1 converge pointwise to χ on [0,1] and do not converge uniformly there (fk(x)=xk+1 converges pointwise but not uniformly on [0,1]).

[L3]

Dini's theorem on a closed interval requires the approximating functions and their pointwise limit to be continuous (Dini's theorem on a closed interval: monotone pointwise convergence of continuous functions to a continuous limit is uniform).

[L4]

Continuity at c requires that every positive output error admit a positive input radius on which all nearby function values remain close to the value at c (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).

Counterexample

technique · direct
1.1

Each fk is continuous by [L2].

L2
1.2

For x∈[0,1], fk+1(x)=xk+2=x xk+1≤xk+1=fk(x), so the sequence is pointwise nonincreasing.

givenalgebra
1.3

The pointwise convergence to χ and the failure of uniform convergence are [L1].

L1
1.4

The function χ is discontinuous at 1: for every δ>0, the point y:=1−min⁡{δ/2,1/2} lies in [0,1) with ∣y−1∣<δ and ∣χ(y)−χ(1)∣=1.

L4algebra
2.1

Thus compactness, continuity of all approximants, and monotonicity hold, but the limit is discontinuous and the uniform conclusion fails; continuity of the limit in [L3] is indispensable.

step 1.1step 1.2step 1.3step 1.4L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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