OAI/Analysis/CircleDomains/Selection/PhysicalSubpaths.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual physical lifts of quotient paths on a compact time interval. The quotient is inverted only where it is a homeomorphism. Constant extension at the interval ends gives an ordinary continuous physical path.

  1. def OAI.CircleDomainRigidity.pathsInsideOn line 18
  2. theorem OAI.CircleDomainRigidity.isOpen_pathsInsideOn line 21
  3. def OAI.CircleDomainRigidity.physicalSubpath line 25
  4. theorem OAI.CircleDomainRigidity.continuous_physicalSubpath line 33
  5. theorem OAI.CircleDomainRigidity.physicalSubpath_mem line 40
  6. theorem OAI.CircleDomainRigidity.physicalSubpath_eq_on line 45
  7. theorem OAI.CircleDomainRigidity.physicalSubpath_comp_clip line 54
  8. theorem OAI.CircleDomainRigidity.physicalSubpath_projects line 70
  9. def OAI.CircleDomainRigidity.totalPhysicalSubpath line 78
  10. theorem OAI.CircleDomainRigidity.measurable_totalPhysicalSubpath line 87