OAI/Geometry/Cannon/Boundary/BoundaryDist.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonReal.expansion_separation line 18
2. abbrev OAI.CannonRelease.boundaryDist line 59
3. lemma OAI.CannonRelease.boundaryDist_le_one line 62
4. lemma OAI.CannonRelease.normalize_closest line 72
5. lemma OAI.CannonMetric.two_far_from_center line 113
6. lemma OAI.CannonRelease.expansion_contraction line 136
7. lemma OAI.CannonRelease.bounded_translate_lipschitz line 156
8. lemma OAI.CannonRelease.proper_triple_word_bound line 169
9. lemma OAI.CannonPaths.joined_avoid_buffer line 235
10. lemma OAI.CannonPaths.isOpen_joined_avoid line 248
11. theorem OAI.CannonPaths.uniform_avoidance line 268