OAI/Analysis/CircleDomains/Selection/BaireRightInverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A continuous surjection from Baire space has a right inverse measurable for any fixed completed finite Borel measure.

  1. theorem OAI.CircleDomainRigidity.exists_nullMeasurable_baire_rightInverse line 11