OAI/Analysis/CircleDomains/Selection/BaireRangeSection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A completed-measure section on the range of a continuous Baire map. The values off the range play no role in the lifting application.

  1. theorem OAI.CircleDomainRigidity.exists_nullMeasurable_baire_rangeSection line 11