A constructive version of the lusin separation theorem

Peter Aczel

pp. 129-151

in: Erik Palmgren, Krister Segerberg (eds), Logicism, intuitionism, and formalism, Berlin, Springer, 2009

Abstract

I state and prove a constructive version of the Lusin Separation Theorem. The classical statement of the theorem is that disjoint analytic sets are Borel separable. The definitions and results are carried out in the axiom system CZF for constructive set theory.