OAI/Geometry/BallPacking/Continuation/ProperPaths.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.freezeTime line 15
2. def OAI.HigherDimensionalBallPacking.Rigidity.frozenPath line 16
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.freezeTime_smooth line 18
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.freezeTime_mem line 21
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.freezeTime_initial line 23
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.freezeTime_final line 25
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.frozenPath_smooth line 27
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.frozen line 30
9. def OAI.HigherDimensionalBallPacking.Rigidity.frozenInitialChart line 64
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.frozenInitialChart_smooth line 90
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.frozenInitialChart_source line 94
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.frozenInitialChart_spatialDerivative line 101
13. def OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.rebase line 118
14. def OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.prescribe line 122
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.SmoothZeroAtlas.prescribe_at line 137
16. theorem OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.smooth_framed_isolating_stabilization line 152
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.IsolatingStabilization.small_frozen_final_collar line 204
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.IsolatingStabilization.small_frozen_initial_collar line 227
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.IsolatingStabilization.small_target_reservoir line 256
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.orientedZeroAtlas_self_source line 281
21. theorem OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.endpoint_exists line 292