OAI/Analysis/CircleDomains/Selection/LastEntryCuts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Last-entry collar cuts and the strict separation of the retained middle fragment from the two endpoint tails.

  1. theorem OAI.CircleDomainRigidity.reversedPath_zero line 17
  2. theorem OAI.CircleDomainRigidity.reversedPath_one line 23
  3. def OAI.CircleDomainRigidity.lastEntryTime line 29
  4. theorem OAI.CircleDomainRigidity.lastEntry_frontier line 32
  5. theorem OAI.CircleDomainRigidity.lastEntry_final_segment line 37
  6. theorem OAI.CircleDomainRigidity.lastEntry_strict_nested line 48
  7. theorem OAI.CircleDomainRigidity.firstExit_lt_lastEntry line 56