Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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.

The indicator of the Cantor set is discontinuous exactly on the Cantor set, which is null, so it is Riemann integrable with integral 0 even though it is discontinuous at uncountably many points

Example

Let C⊆[0,1] be the Cantor middle-thirds set (The Cantor middle-thirds set as the intersection of the sets Cn obtained by removing open middle thirds) and let 1C:[0,1]→R be its indicator, 1C(x)=1 for x∈C and 1C(x)=0 otherwise. Then:

  1. 1C is discontinuous at every point of C and continuous at every point of [0,1]∖C, so its set of discontinuities is exactly 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, Discontinuity of f at a point of its domain, and its classification: removable discontinuity, jump discontinuity and essential discontinuity, equivalently Rudin's discontinuities of the first and of the second kind);
  2. 1C is Riemann integrable on [0,1], because C has measure zero (The Cantor set is compact, perfect, uncountable, nowhere dense and of measure zero, and it contains no interval of positive length, so its only nonempty connected subsets are single points, Lebesgue's criterion for Riemann integrability: a bounded f on [a,b] is Riemann integrable if and only if its set of discontinuities has measure zero);
  3. ∫011C=0.

The point of the example is claim 2 against claim 1. The discontinuity set is uncountable (The Cantor set is compact, perfect, uncountable, nowhere dense and of measure zero, and it contains no interval of positive length, so its only nonempty connected subsets are single points, Finite, countably infinite, countable, uncountable), so no cardinality argument such as A bounded function on [a,b] whose set of discontinuities is at most countable is Riemann integrable applies; what makes the function integrable is that C can be covered by intervals of arbitrarily small total length, and nothing else.

Only the implication "measure zero ⇒ integrable" of Lebesgue's criterion for Riemann integrability: a bounded f on [a,b] is Riemann integrable if and only if its set of discontinuities has measure zero is used, so no choice principle is involved.

Facts & Assumptions

Given: The Cantor set C⊆[0,1] and its indicator 1C:[0,1]→R.

[L3]

A bounded f on [a,b] with a<b is Riemann integrable if and only if its set of discontinuities has measure zero; the implication from "measure zero" to "integrable" uses no choice principle (Lebesgue's criterion for Riemann integrability: a bounded f on [a,b] is Riemann integrable if and only if its set of discontinuities has measure zero, Lower bound, bounded below, bounded set).

[L6]

A set with a least element has it as its infimum; the supremum of {0} is 0 (Greatest lower bound (infimum), Maximum and minimum of a set, Complete ordered field (least-upper-bound property)).

[L8]

Ordered-field arithmetic: for 0≤x≤1 and a real ρ>0 the reals u:=max⁡{0,x−ρ} and v:=min⁡{1,x+ρ} satisfy u<v and (u,v)⊆Nρ(x)∩[0,1] (Maximum and minimum of a set, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property), The ε-neighbourhood and the punctured ε-neighbourhood of a point of R, Intervals of R: the nine order-convex forms, nondegeneracy, and length). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Verification

technique · direct
1.1

1C takes only the values 0 and 1, so it is bounded on [0,1] and its Darboux sums and integrals are defined by [L5].

givenL5
1.2

Discontinuity on C. Let x∈C, so 1C(x)=1, and let a real ρ>0 be given. By [L8] the set (u,v)⊆Nρ(x)∩[0,1] is a nonempty open interval, so by [L1] it contains a point y∉C; then y∈[0,1], ∣y−x∣<ρ and ∣1C(x)−1C(y)∣=1. So the continuity condition fails at x for ε:=1.

givenL1L8
1.3

Continuity off C. Let x∈[0,1] with x∉C. Since C is closed, [L2] gives a real ρ>0 with Nρ(x)∩C=∅, so 1C vanishes on Nρ(x)∩[0,1] and ∣1C(y)−1C(x)∣=0<ε there for every ε>0.

givenL1L2
2.1

So the set of discontinuities of 1C in [0,1] is exactly C, which has measure zero by [L1]; by [L3] and 0<1, 1C is Riemann integrable on [0,1].

step 1.1step 1.2step 1.3L1L3
2.2

Every lower sum is 0. Let P=(n,t) be a partition of [0,1] and i<n. By [L4] the interval (ti,ti+1) is a nonempty open subset of [0,1], so by [L1] it contains a point outside C, at which 1C takes the value 0; since 1C≥0, the value 0 is the least element of 1C[Ii] and mi=0 by [L6]. Hence L(1C,P)=0 by [L5] and [L7].

step 1.1L1L4L5L6L7
3.1

The set of lower sums is {0}, so ∫01‾1C=0 by [L6]; and 1C is integrable by step 2.1, so ∫011C=0 by [L5].

step 2.1step 2.2L5L6∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

85 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