OAI/Analysis/CircleDomains/Topology/CountablePathConcatenation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Actual countable path concatenation, including the new limiting endpoint. The shrinking-tail hypothesis is the one supplied by nested dust collars.

  1. def OAI.CircleDomainRigidity.collarPieceIndex line 17
  2. theorem OAI.CircleDomainRigidity.collarPieceIndex_spec line 20
  3. def OAI.CircleDomainRigidity.collarPiece line 25
  4. theorem OAI.CircleDomainRigidity.collarPiece_lower line 28
  5. theorem OAI.CircleDomainRigidity.collarPiece_upper line 35
  6. theorem OAI.CircleDomainRigidity.collarPieces_agree line 42
  7. def OAI.CircleDomainRigidity.collarConcatenationFun line 59
  8. theorem OAI.CircleDomainRigidity.collarConcatenation_on_cell line 62
  9. theorem OAI.CircleDomainRigidity.collarConcatenation_continuous_positive line 71
  10. theorem OAI.CircleDomainRigidity.collarConcatenation_continuous line 82
  11. def OAI.CircleDomainRigidity.collarConcatenation line 115
  12. theorem OAI.CircleDomainRigidity.collarConcatenation_zero line 120
  13. theorem OAI.CircleDomainRigidity.collarConcatenation_affine line 124
  14. theorem OAI.CircleDomainRigidity.collarConcatenation_one line 134