OAI/Analysis/CircleDomains/Selection/LastEntryFragmentProperties.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Final fragment endpoints lie on their actual collars and carry zero cut toll whenever the collars do.

  1. theorem OAI.CircleDomainRigidity.lastEntryFragmentArray_frontiers line 18
  2. theorem OAI.CircleDomainRigidity.lastEntry_toll_zero line 37