OAI/Analysis/CircleDomains/Topology/PathLoopErasure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Removing a closed loop preserves every modulus of continuity and cannot increase the diameter on any parameter interval.

  1. def OAI.CircleDomainRigidity.erasePathLoop line 19
  2. lemma OAI.CircleDomainRigidity.erasePathLoop_of_le line 33
  3. lemma OAI.CircleDomainRigidity.erasePathLoop_of_mem line 37
  4. lemma OAI.CircleDomainRigidity.erasePathLoop_of_ge line 41
  5. lemma OAI.CircleDomainRigidity.erasePathLoop_pair line 47
  6. lemma OAI.CircleDomainRigidity.unitInterval_dist_le_of_mem_Icc line 73