OAI/Analysis/CircleDomains/Topology/DyadicPathReplacement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Replace a finely subdivided map by a path whose endpoints lie in a fixed set, preserving a uniform error and a prescribed neighborhood.

  1. def OAI.CircleDomainRigidity.halfTime line 12
  2. lemma OAI.CircleDomainRigidity.leftHalf_zero line 13
  3. lemma OAI.CircleDomainRigidity.leftHalf_one line 14
  4. lemma OAI.CircleDomainRigidity.rightHalf_zero line 15
  5. lemma OAI.CircleDomainRigidity.rightHalf_one line 16
  6. lemma OAI.CircleDomainRigidity.dyadic_path_replacement line 18