OAI/Analysis/CircleDomains/Selection/FirstExitFragmentGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ordering and support of the actual first-exit fragments in nested collars. The order gives disjoint open time intervals for the cost budget.

  1. theorem OAI.CircleDomainRigidity.antitone_interval_interiors line 16
  2. theorem OAI.CircleDomainRigidity.firstExitTime_antitone line 27
  3. theorem OAI.CircleDomainRigidity.firstExitFragments_disjoint line 34
  4. theorem OAI.CircleDomainRigidity.firstExitFragments_strict line 39