Functions of Baire Class One over a Bishop Topology

If [Formula: see text] is a topology of open sets on a set X, a real-valued function on X is of Baire class one over [Formula: see text], if it is the pointwise limit of a sequence of functions in the corresponding ring of continuous functions C(X). If F is a Bishop topology of functions on X, a constructive and function-theoretic alternative to [Formula: see text] introduced by Bishop, we define a real-valued function on X to be of Baire class one over F, if it is the pointwise limit of a sequence of functions in F. We show that the set [Formula: see text] of functions of Baire class one over a given Bishop topology F on a set X is a Bishop topology on X. Consequently, notions and results from the general theory of Bishop spaces are naturally translated to the study of Baire class one-functions. We work within Bishop’s informal system of constructive mathematics [Formula: see text], that is [Formula: see text] extended with inductive definitions with rules of countably many premises.