Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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.

Baire's theorem: a Baire class one function on a closed bounded interval [a,b] is continuous at the points of a dense subset of [a,b] that is the trace of a Gδ set, so its set of discontinuities is meager

Statement

Let a,b∈R with a<b and let f:[a,b]→R be of Baire class one (Pointwise convergence of a sequence of real functions, and the Baire class one functions as the pointwise limits of sequences of continuous functions). Write

D  :=  { x∈[a,b]:f is discontinuous at x },C:=[a,b]∖D

(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:

  1. for every real ε>0 the set Dε:={ x∈[a,b]:ωf(x)≥ε } (The oscillation ωf(S)=sup⁡{ ∣f(x)−f(y)∣:x,y∈S } of f on a set and the oscillation ωf(c)=inf⁡δ>0ωf(A∩Nδ(c)) at a point, both taken in the extended reals) is a closed subset of R containing no nondegenerate closed interval, hence nowhere dense (Nowhere dense, meager (first category), residual, and second category subsets of R);
  2. D is meager, being the union of the sequence (D1/ι(n+1))n∈N of nowhere dense sets;
  3. C is dense in [a,b]: for every x∈[a,b] and every real ρ>0 the set [a,b]∩Nρ(x) contains a point of C;
  4. C=[a,b]∩V for a Gδ subset V⊆R (Fσ and Gδ subsets of R).

On the phrase "dense Gδ". Claims 3 and 4 together are what the classical statement calls a dense Gδ subset of [a,b]: the continuity set is dense in [a,b] and it is the trace on [a,b] of a Gδ subset of R. It is not claimed that C is Gδ as a subset of R, nor that it is dense in R; neither is true in general, since C⊆[a,b].

Facts & Assumptions

Given: Reals a<b, a function f:[a,b]→R of Baire class one, and a sequence (fk)k∈N of continuous functions on [a,b] converging pointwise to f.

[L2]

ωf(S)=sup⁡{∣f(x)−f(y)∣:x,y∈S}; ωf(x)=inf⁡{ωf([a,b]∩Nδ(x)):δ>0}; ωf is monotone under inclusion and ωf(x)≥0 (The oscillation ωf(S)=sup⁡{ ∣f(x)−f(y)∣:x,y∈S } of f on a set and the oscillation ωf(c)=inf⁡δ>0ωf(A∩Nδ(c)) at a point, both taken in the extended reals).

[L4]

For every real ε>0 there is a closed G⊆R with {x∈[a,b]:ωf(x)≥ε}=[a,b]∩G (For every real ε>0 the set { x∈A:ωf(x)≥ε } is the intersection with A of a closed subset of R; in particular it is closed in R when A=R).

[L5]

If a<b, (Fn) are closed and [a,b]⊆⋃nFn, then some Fn∩[a,b] contains a nondegenerate closed interval (Baire category inside a closed bounded interval: if [a,b] with a<b is covered by a sequence of closed sets, then one of them contains a nondegenerate closed subinterval of [a,b]; no choice principle is used).

[L6]

[a,b] and every [c,d] with c≤d are closed; an intersection of a nonempty family of closed sets is closed; a set is closed exactly when its complement is open (Arbitrary unions and finite intersections of open subsets of R are open, and dually for closed sets, claim 3, Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Intervals of R: the nine order-convex forms, nondegeneracy, and length).

[L9]

The set of continuity points of f:A→R is A∩V for a Gδ set V⊆R, and the discontinuity set is {x∈A:ωf(x)>0}=⋃n∈N{x∈A:ωf(x)≥1/ι(n+1)} (For f:A→R the set of points of A at which f is discontinuous is the intersection with A of an Fσ subset of R, and the set of points at which f is continuous is the intersection with A of a Gδ subset; for A=R the two sets are Fσ and Gδ outright, claims 1 and 2, Fσ and Gδ subsets of R).

[L11]

∣u−w∣≤∣u−v∣+∣v−w∣, ∣u∣≥0, and a real that is ≤η for every real η>0 and ≥0 is 0 (Basic properties of the absolute value).

Proof

technique · direct
1.1

Refinement claim. Let [c,d]⊆[a,b] with c<d and let ε>0 be real. For N∈N put EN:={ x∈[c,d]:∣fn(x)−fm(x)∣≤ε/4 for all n,m≥N }.

L1construct
1.2

Claim 1. Fix a real ε>0 and let Dε:={x∈[a,b]:ωf(x)≥ε}. It is closed in R, being [a,b]∩G with G closed and [a,b] closed.

L4L6
1.3

Claim 4. The set of continuity points of f on the domain [a,b] is [a,b]∩V for a Gδ subset V⊆R.

L9
1.4

Claim 3. Let x∈[a,b] and let ρ>0 be real. The set [a,b]∩Nρ(x) contains a nondegenerate closed interval [c,d] with c<d, because a<b: taking c:=max⁡{a, x−ρ/2} and d:=min⁡{b, x+ρ/2} gives [c,d]⊆[a,b]∩Nρ(x) and c<d: if x=a then c=a and d=min⁡{b,a+ρ/2}>a; if x=b then d=b and c=max⁡{a,b−ρ/2}<b; and if a<x<b then c<x<d.

L12
2.1

Each EN is closed: for fixed n,m the set {x∈[c,d]:∣fn(x)−fm(x)∣≤ε/4} is the preimage under the continuous function ∣fn−fm∣ of the closed set {y:y≤ε/4}, hence of the form G∩[c,d] with G closed, hence closed since [c,d] is; and EN is the intersection of that nonempty family of closed sets over the pairs n,m≥N.

step 1.1L6L7
2.2

[c,d]=⋃N∈NEN: for x∈[c,d] the sequence (fk(x)) converges to f(x), so there is N with ∣fk(x)−f(x)∣<ε/8 for all k≥N, and then ∣fn(x)−fm(x)∣≤∣fn(x)−f(x)∣+∣f(x)−fm(x)∣<ε/4 for all n,m≥N.

step 1.1L1L11
3.1

By the interval form of Baire category applied to [c,d] and the sequence (EN), there are N∈N and reals u′<v′ with [u′,v′]⊆EN∩[c,d]=EN.

step 1.1step 2.1step 2.2L5
4.1

For every x∈[u′,v′] one has ∣fN(x)−f(x)∣≤ε/4. Indeed, let η>0 be real; since fm(x)→f(x) there is m≥N with ∣fm(x)−f(x)∣<η, and then ∣fN(x)−f(x)∣≤∣fN(x)−fm(x)∣+∣fm(x)−f(x)∣<ε/4+η; as η>0 was arbitrary this gives ∣fN(x)−f(x)∣≤ε/4.

step 1.1step 3.1L1L11
4.2

Put x0:=(u′+v′)/2, so u′<x0<v′. Since fN is continuous at x0 there is a real δ>0 with ∣fN(x)−fN(x0)∣<ε/4 for every x∈[a,b] with ∣x−x0∣<δ. Put u:=max⁡{u′, x0−δ/2} and v:=min⁡{v′, x0+δ/2}, so that u<x0<v and [u,v]⊆[u′,v′] with ∣x−x0∣<δ for every x∈[u,v].

step 3.1L1L12
5.1

For x,y∈[u,v]: ∣f(x)−f(y)∣≤∣f(x)−fN(x)∣+∣fN(x)−fN(x0)∣+∣fN(x0)−fN(y)∣+∣fN(y)−f(y)∣≤ε/4+ε/4+ε/4+ε/4=ε. Hence ωf([u,v])≤ε, ε being an upper bound of the set whose supremum that is.

step 4.1step 4.2L2L11
6.1

The refinement claim is proved: for every [c,d]⊆[a,b] with c<d and every real ε>0 there are u<v with [u,v]⊆[c,d] and ωf([u,v])≤ε. Moreover every x with u<x<v satisfies ωf(x)≤ε, since [a,b]∩Nρ(x)⊆[u,v] for ρ:=min⁡{x−u, v−x}>0 and ωf is monotone under inclusion.

step 4.2step 5.1L2L12
7.1

Dε contains no nondegenerate closed interval. Were [c,d]⊆Dε with c<d, the refinement claim applied to [c,d] and to the positive real ε/2 would give u<v with [u,v]⊆[c,d] and ωf(x)≤ε/2<ε for every x with u<x<v; such an x lies in [c,d]⊆Dε and so satisfies ωf(x)≥ε, which is impossible.

step 6.1step 1.2
8.1

Hence Dε is nowhere dense: it is closed, so it equals its own closure, and its interior is empty, since an interior point would have a neighbourhood Nρ(x)⊆Dε and then [x−ρ/2, x+ρ/2] would be a nondegenerate closed interval inside Dε.

step 1.2step 7.1L8L12
9.1

Claim 2. D=⋃n∈ND1/ι(n+1), and each D1/ι(n+1) is nowhere dense by step 8.1, so D is a union of a sequence of nowhere dense sets, that is, meager.

step 8.1L8L9L10
10.1

Suppose [c,d]⊆D with c<d as in step 1.4. Then [c,d] is covered by the sequence (D1/ι(n+1)) of closed sets, so by the interval form of Baire category some D1/ι(n+1)∩[c,d] contains a nondegenerate closed interval, contradicting step 7.1. So [c,d]⊈D, and any point of [c,d]∖D is a point of C inside [a,b]∩Nρ(x).

step 7.1step 9.1step 1.4L5L6
11.1

Claims 1, 2, 3 and 4 are therefore proved: claim 1 by steps 1.2, 7.1 and 8.1, claim 2 by step 9.1, claim 3 by steps 1.4 and 10.1, and claim 4 by step 1.3.

step 8.1step 9.1step 1.3step 10.1∎

Remarks

Depends on

Used by

Dependency tree · two levels

58 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