OAI/Analysis/CircleDomains/Topology/JoinedPhysicalPaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Binary joining preserves finite physical length and adds the exact physical occupation costs.

  1. def OAI.CircleDomainRigidity.collarRestrictions line 18
  2. theorem OAI.CircleDomainRigidity.collarRestrictions_length_sum line 22
  3. def OAI.CircleDomainRigidity.joinedPhysicalPieces line 29
  4. theorem OAI.CircleDomainRigidity.joinedPhysicalPieces_match line 34
  5. theorem OAI.CircleDomainRigidity.joinedPhysicalPieces_length_sum line 45
  6. def OAI.CircleDomainRigidity.joinedFinitePhysicalPath line 53
  7. theorem OAI.CircleDomainRigidity.collarRestrictions_cost_sum line 63
  8. theorem OAI.CircleDomainRigidity.physicalCost_joined line 70