Borel and Baire Sets in Bishop Spaces

摘要

We study the Borel sets Borel(F) and the Baire sets Baire(F) generated by a Bishop topology F on a set X. These are inductively defined sets of F-complemented subsets of X. Because of the constructive definition of Borel(F), and in contrast to classical topology, we show that Baire(F) = Borel(F). We define the uniform version of an F-complemented subset of X and we show the Urysohn lemma for them. We work within Bishop's system BISH* of informal constructive mathematics that includes inductive definitions with rules of countably many premises.