OAI/Analysis/CircleDomains/Topology/CountablePathTimes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Decreasing dyadic intervals for the countable collar concatenation.

  1. def OAI.CircleDomainRigidity.collarTime line 16
  2. theorem OAI.CircleDomainRigidity.collarTime_pos line 19
  3. theorem OAI.CircleDomainRigidity.collarTime_zero line 23
  4. theorem OAI.CircleDomainRigidity.collarTime_strictAnti line 27
  5. theorem OAI.CircleDomainRigidity.collarTime_tendsto line 34
  6. theorem OAI.CircleDomainRigidity.exists_collarTime_cell line 38
  7. def OAI.CircleDomainRigidity.collarCell line 45
  8. theorem OAI.CircleDomainRigidity.collarCell_disjoint_interiors line 47
  9. theorem OAI.CircleDomainRigidity.collarCell_complement_countable line 58
  10. abbrev OAI.CircleDomainRigidity.PositivePathTime line 72
  11. theorem OAI.CircleDomainRigidity.collarCells_locallyFinite line 74
  12. theorem OAI.CircleDomainRigidity.collarCells_cover_positive line 89