OAI/Analysis/CircleDomains/Topology/InterleavedCollarPieces.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Interleaving actual retained fragments with their joining arcs preserves the endpoint matches and adds exactly the two series of costs.

  1. def OAI.CircleDomainRigidity.interleavePieces line 15
  2. theorem OAI.CircleDomainRigidity.interleavePieces_even line 18
  3. theorem OAI.CircleDomainRigidity.interleavePieces_odd line 21
  4. theorem OAI.CircleDomainRigidity.interleavePieces_join line 24
  5. theorem OAI.CircleDomainRigidity.interleavePieces_tail line 39
  6. theorem OAI.CircleDomainRigidity.tsum_interleavePieces line 56
  7. theorem OAI.CircleDomainRigidity.tsum_cost_interleavePieces line 61