OAI/Analysis/KadisonKastler/PublishedBorelSelection.lean

The published Borel selection input

Alexander S. Kechris, Classical Descriptive Set Theory, GTM 156, Springer (1995), Theorem 18.1, pp.120–121, and Theorem 21.10, pp.155–156. DOI: 10.1007/978-1-4612-4190-4.

We retain only selection for Borel relations whose second coordinate is the proved Polish unitary coordinate space, for one finite Borel measure. The published universally measurable selector is measurable for the completed measure, hence has the AEMeasurable formulation used here. No algebra-conjugacy or perturbation conclusion is part of this input.