OAI/Analysis/CircleDomains/Topology/JoinedPaths.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A binary continuous join with exact affine parametrizations of both halves, for attaching collar tails to retained fragments.

  1. def OAI.CircleDomainRigidity.joinedPath line 18
  2. theorem OAI.CircleDomainRigidity.joinedPath_first line 21
  3. theorem OAI.CircleDomainRigidity.joinedPath_second line 38
  4. theorem OAI.CircleDomainRigidity.joinedPath_collar_succ line 63
  5. theorem OAI.CircleDomainRigidity.joinedPath_zero line 78
  6. theorem OAI.CircleDomainRigidity.joinedPath_one line 82