OAI/Geometry/BallPacking/Degree/EuclideanAtlasTransport.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedModelAtlas line 15
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.conjugate_clm_det line 28
3. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedModelAtlas.toCoordinates line 33
4. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.timeSpaceCoordinates line 69
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.timeSpaceCoordinates_apply line 88
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.timeSpaceCoordinates_symm_apply line 90
7. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.initialCollarDensity line 100
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.initialCollarDensity_continuous line 103
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.initialCollarDensity_support line 108
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.initialCollarDensity_compact line 119
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.initialCollarDensity_integral_pos line 129
12. theorem OAI.HigherDimensionalBallPacking.Rigidity.Degree.collar_stokes_contradiction line 147
13. structure OAI.HigherDimensionalBallPacking.Rigidity.Degree.ModelAtlasSmoothMap line 195
14. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.ModelAtlasSmoothMap.toCoordinates line 200
15. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasSmoothMap.restrict line 206
16. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasSmoothMap.comp line 218
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedSmoothAtlas.finite_inside line 230
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.small_inverse_bump line 257
19. theorem OAI.HigherDimensionalBallPacking.Rigidity.Degree.isolated_collar_impossible line 278