Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge 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.

Pointwise convergence of a sequence of real functions, and the Baire class one functions as the pointwise limits of sequences of continuous functions

Definition

Let A⊆R. A sequence of functions on A is a function assigning to each n∈N a function fn:A→R; it is written (fn)n∈N. As everywhere in this library N contains 0, so the first term is f0 (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Pointwise convergence. (fn) converges pointwise on A to f:A→R when, for every x∈A, the sequence of reals (fn(x))n∈N converges to f(x) (Limits and Cauchy sequences of reals); written out, for every x∈A and every real ε>0 there is N∈N with ∣fn(x)−f(x)∣<ε for every n≥N.

The limit function is unique. A sequence of reals has at most one limit (A sequence has at most one limit), so if (fn) converges pointwise to f and to g then f(x)=g(x) for every x∈A, hence f=g. We may therefore speak of the pointwise limit and write f=lim⁡nfn pointwise.

The index N is allowed to depend on x, and that is the whole content of the word pointwise. No uniformity over A is asserted anywhere below.

Baire class one

f:A→R is of Baire class one on A when there is a sequence (fn) of functions A→R, each continuous on A (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), converging pointwise on A to f.

Every continuous function is of Baire class one, by the constant sequence fn:=f, which converges pointwise to f because a constant sequence of reals converges to its value.

The class is strictly larger than the continuous functions, and it is strictly smaller than the class of all functions. The first is visible already on A=[0,1] (Intervals of R: the nine order-convex forms, nondegeneracy, and length): the indicator of a single point is of Baire class one and is not continuous. The second is 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, which shows that a Baire class one function on a closed bounded interval has a dense set of continuity points, and the companion page uses it to exhibit a function that is not of Baire class one.

On the higher classes. The pointwise limits of sequences of Baire class one functions form what is classically called Baire class two, and the construction iterates. No definition of the higher classes is given here and none is used; where the phrase is needed below it is stated as "a pointwise limit of a sequence of Baire class one functions", which is a condition already expressible with the words above.

Depends on

Used by

Dependency tree · two levels

25 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