OAI/Analysis/CircleDomains/Topology/ReversedBoundaryTolls.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dust tolls under reversal, including the two distinct endpoint conventions used for collar fragments and one-ended paths.

  1. theorem OAI.CircleDomainRigidity.boundaryToll_reversed line 18
  2. theorem OAI.CircleDomainRigidity.preterminalToll_reversed_add_initial line 22
  3. theorem OAI.CircleDomainRigidity.preterminalToll_reversed_of_zero_endpoints line 31
  4. theorem OAI.CircleDomainRigidity.interiorToll_reversed line 36