OAI/Analysis/CircleDomains/Topology/PathSelectionInput.lean

Published input for the compact-arc reduction: Kechris, Classical Descriptive Set Theory (1995), Theorem 18.1, p.120, and Theorem 29.9, p.227. We use only Borel relations between sphere path spaces with all sections nonempty, and measurability after completing one probability law.