OAI/Analysis/CircleDomains/Topology/AffinePathTime.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Increasing affine restriction maps and their clipped inverse on the standard path interval. Interior inequalities remain exact after clipping.

  1. def OAI.CircleDomainRigidity.affinePathTime line 16
  2. theorem OAI.CircleDomainRigidity.affinePathTime_coe line 23
  3. theorem OAI.CircleDomainRigidity.affinePathTime_zero line 28
  4. theorem OAI.CircleDomainRigidity.affinePathTime_one line 31
  5. theorem OAI.CircleDomainRigidity.affinePathTime_strictMono line 34
  6. theorem OAI.CircleDomainRigidity.affinePathTime_mem_Icc line 43
  7. def OAI.CircleDomainRigidity.rescalePathTime line 54
  8. theorem OAI.CircleDomainRigidity.rescalePathTime_coe line 58
  9. theorem OAI.CircleDomainRigidity.rescale_affinePathTime line 61
  10. theorem OAI.CircleDomainRigidity.affine_rescalePathTime line 70
  11. theorem OAI.CircleDomainRigidity.range_affinePathTime line 83
  12. theorem OAI.CircleDomainRigidity.rescalePathTime_lt_iff line 91
  13. theorem OAI.CircleDomainRigidity.lt_rescalePathTime_iff line 102