OAI/Analysis/CircleDomains/Probability/MeasurableRaySides.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Both sides have analytic path descriptions, so their membership sets are Borel by Suslin's theorem. This avoids a measurable Schoenflies choice.

  1. theorem OAI.CircleDomainRigidity.isClosed_pathPairMeet line 16
  2. theorem OAI.CircleDomainRigidity.analyticSet_diskAvoidingPath line 37
  3. theorem OAI.CircleDomainRigidity.measurableSet_rayRightFamily line 76