OAI/Geometry/BallPacking/Fredholm/SurjectiveParametricReduction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.surjective_package_coker_subsingleton line 23
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricSolution_kernel_coordinate line 34
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.parametricSolution_graph_injective line 39
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.surjective_parametricSolution_zero line 48
5. theorem OAI.HigherDimensionalBallPacking.Rigidity.surjective_zero_chart line 56
6. def OAI.HigherDimensionalBallPacking.Rigidity.augmentedCokerMap line 84
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.augmented_kernel_coker_zero line 89
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.augmented_kernel_first_coordinate line 98
9. def OAI.HigherDimensionalBallPacking.Rigidity.augmentedKernelRead line 108
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.augmentedKernelRead_injective line 120
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.augmentedKernelRead_surjective line 131
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.augmentedCokerMap_surjective line 151
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.augmentedKernel_finrank line 164
14. structure OAI.HigherDimensionalBallPacking.Rigidity.FiniteZeroGerm line 190
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.finiteZeroGerm_of_surjective line 202
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.finiteTargetAugment_zero_germ line 216
17. theorem OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.stabilized_zero_germs line 234
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.stabilized_initial_graph line 254
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.surjective_fredholm_right_inverse line 280
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.local_continuous_right_inverse line 296
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_continuous_right_inverse line 318
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.cylinder_supplement line 372
23. def OAI.HigherDimensionalBallPacking.Rigidity.splitKernelProjection line 399
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.splitKernelProjection_apply line 403
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.splitKernelProjection_mem_ker line 408
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.splitKernelProjection_fixed line 416
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.splitKernelProjection_idempotent line 421
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.splitKernelProjection_range line 428
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.ProperIndexZeroPath.cylinder_kernel_projection line 437
30. def OAI.HigherDimensionalBallPacking.Rigidity.projectionTransport line 481
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTransport_self line 485
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTransport_comp line 493
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.comp_projectionTransport line 501
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTransport_intertwines line 508
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTransport_fixed line 512
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTransport_fixed_surjective line 518
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.projectionTransport_continuousOn line 529
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_projection_transport line 534