OAI/Geometry/BallPacking/Moduli/ZeroCharts.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart line 16
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.FiniteZeroGerm.graphChart line 34
3. def OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.inverse line 65
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.inverse_val line 70
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.inverse_continuousOn line 73
6. def OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.partialHomeomorph line 83
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.base_mem_source line 109
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.partialHomeomorph_apply line 112
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.partialHomeomorph_symm_val line 115
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.transition_smooth line 119
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.transition_eq line 124
12. def OAI.HigherDimensionalBallPacking.Rigidity.StabilizedKernelFrame.kernelEquiv line 140
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.StabilizedKernelFrame.fredholm line 155
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.StabilizedKernelFrame.zero_germ line 170
15. def OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.reparam line 196
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.FiniteZeroGerm.common_graphChart line 225
17. def OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.spatialDerivative line 244
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.spatialDerivative_continuous line 248
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.hasSpatialDerivative line 252
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.spatialDerivative_coordinate line 258
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.spatialDerivative_injective line 267
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.ZeroGraphChart.spatialDerivative_kernel line 275
23. def OAI.HigherDimensionalBallPacking.Rigidity.framedChartJacobian line 302
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedChartJacobian_injective line 305
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedChartJacobian_bijective line 318
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedChartJacobian_det_ne_zero line 324
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedChartJacobian_continuous line 332
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedChart_orientation_neighborhood line 341
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.zeroChart_transition_derivative line 369
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedChart_transition_identity line 398
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedChart_transition_det line 410
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedChart_transition_signed_det line 420
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.smooth_actual_implicit_branch line 454
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.implicitFunction_smooth_neighborhood line 471