OAI/Geometry/BallPacking/Fredholm/ProjectionTimeGrid.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.cappedTime line 15
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.cappedTime_continuous line 17
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.cappedTime_mem line 20
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.cappedTime_zero line 24
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.cappedTime_last line 27
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.cappedTime_step line 31
7. def OAI.HigherDimensionalBallPacking.Rigidity.projectionTimeChain line 49
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTimeChain_continuousOn line 54
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTimeChain_intertwines line 68
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTimeChain_invertible line 80
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_projection_time_transport line 94
12. def OAI.HigherDimensionalBallPacking.Rigidity.cappedTimeMap line 110
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.cappedTimeMap_continuous line 112
14. def OAI.HigherDimensionalBallPacking.Rigidity.gridDomain line 115
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.gridDomain_open line 118
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.gridDomain_time_mem line 123
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.gridDomain_contains line 128
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTimeChain_continuousOn_grid line 136
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTimeChain_intertwines_grid line 149
20. def OAI.HigherDimensionalBallPacking.Rigidity.extendedTimeTransport line 165
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.extendedTimeTransport_continuousOn line 169
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.extendedTimeTransport_intertwines line 181
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.extendedTimeTransport_eq_chain line 196
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_kernel_transport_neighborhood line 205
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.pathSpatialDerivative_initial line 241
26. def OAI.HigherDimensionalBallPacking.Rigidity.initialKernelGraph line 249
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialKernelGraph_apply line 253
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialKernelGraph_kernel line 257
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.projection_fixed_iff_range line 272
30. structure OAI.HigherDimensionalBallPacking.Rigidity.StabilizedKernelFrame line 279
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.stabilized_kernel_frame line 290