OAI/Analysis/CircleDomains/Selection/TaggedPhysicalRestriction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual affine restrictions of tagged finite-physical paths, retaining all the tag and physical-cost information used by the collar fragments.

  1. def OAI.CircleDomainRigidity.restrictTaggedPhysicalPath line 19
  2. theorem OAI.CircleDomainRigidity.restrictTaggedPhysicalPath_zero line 25
  3. theorem OAI.CircleDomainRigidity.restrictTaggedPhysicalPath_one line 33
  4. theorem OAI.CircleDomainRigidity.restrictTaggedPhysicalPath_range line 41
  5. theorem OAI.CircleDomainRigidity.restrictTaggedPhysicalPath_allowed line 50