If T is a topology of open sets on a set X, a real-valued function on X is of Baire class one over T, if it is the pointwise limit of a sequence of functions in the corresponding ring of continuous functions C(Ⅹ). If F is a Bishop topology of functions on A", a constructive and function-theoretic alternative to T 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 B_1 (F) 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 BISH*, that is BISH extended with inductive definitions with rules of countably many premises.
展开▼
