OAI/Analysis/CircleDomains/Selection/FirstExitCuts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual first-exit cuts for the collar-splicing construction. Every retained initial fragment lies in the corresponding closed collar disk.

  1. def OAI.CircleDomainRigidity.firstExitTime line 18
  2. theorem OAI.CircleDomainRigidity.firstExitTime_le line 21
  3. theorem OAI.CircleDomainRigidity.mem_before_firstExit line 25
  4. theorem OAI.CircleDomainRigidity.firstExit_notMem line 30
  5. theorem OAI.CircleDomainRigidity.firstExit_pos line 34
  6. theorem OAI.CircleDomainRigidity.firstExit_frontier line 40
  7. theorem OAI.CircleDomainRigidity.firstExit_initial_segment line 50
  8. theorem OAI.CircleDomainRigidity.firstExit_nested line 59
  9. theorem OAI.CircleDomainRigidity.firstExit_strict_nested line 65