OAI/Geometry/Cannon/Flows/IntervalAvoidingShortRange.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonPairs.interval_avoiding_short_range line 21
2. lemma OAI.CannonPairs.cells_into_puncture_exterior line 38
3. theorem OAI.CannonPairs.path_forces_opposite_oscillation line 63
4. lemma OAI.CannonPairs.separated_paths_avoid_short_range line 137
5. theorem OAI.CannonPairs.two_path_pair_alternative line 170
6. lemma OAI.CannonPairs.uniformly_on_preimage line 225
7. lemma OAI.CannonPairs.continuousOn_preimage line 233
8. lemma OAI.CannonPairs.puncture_exterior_domain line 238
9. lemma OAI.CannonPairs.pattern_puncture_distance line 258
10. lemma OAI.CannonPairs.wide_image_enters line 277
11. theorem OAI.CannonPairs.transformed_level_paths line 294
12. theorem OAI.CannonPairs.fixed_source_pair line 341