OAI/Analysis/CircleDomains/Selection/FirstExitFragmentArray.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual triangular array of initial collar fragments. Entries before the relevant collar is reached use the old path and are never selected.

  1. def OAI.CircleDomainRigidity.firstExitFragmentArray line 18
  2. theorem OAI.CircleDomainRigidity.firstExitFragmentArray_eq line 25
  3. theorem OAI.CircleDomainRigidity.firstExitFragmentArray_endpoints line 34
  4. theorem OAI.CircleDomainRigidity.firstExitFragmentArray_support line 46
  5. theorem OAI.CircleDomainRigidity.firstExitFragmentArray_allowed line 63