OAI/Analysis/CircleDomains/Topology/AllowedCollarConcatenation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The constructed countable collar path is allowed when its actual physical lengths are summable. No path-stability input is assumed.

  1. def OAI.CircleDomainRigidity.collarTaggedPath line 19
  2. theorem OAI.CircleDomainRigidity.allowedTaggedPath_collar line 25