OAI/Analysis/CircleDomains/Topology/DomainPhysicalPaths.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A rectifiable physical path entirely in the original domain projects to an allowed quotient path, with exactly its original physical length.

  1. def OAI.CircleDomainRigidity.projectDomainPath line 18
  2. theorem OAI.CircleDomainRigidity.projectDomainPath_mem line 23
  3. theorem OAI.CircleDomainRigidity.physicalDyadicPath_project line 26
  4. theorem OAI.CircleDomainRigidity.physicalStageLength_project line 37
  5. theorem OAI.CircleDomainRigidity.physicalDomainLength_project line 50
  6. theorem OAI.CircleDomainRigidity.projected_physical_path_allowed line 57