OAI/GroupTheory/UniversalGroup/CellRetractions.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniversalFInfinity.GeneralPosition.lipschitz_mul line 18
2. def OAI.UniversalFInfinity.GeneralPosition.lipschitzAlgebra line 39
3. lemma OAI.UniversalFInfinity.GeneralPosition.lipschitzAlgebra_separates line 47
4. lemma OAI.UniversalFInfinity.GeneralPosition.exists_lipschitz_approximation line 53
5. lemma OAI.UniversalFInfinity.GeneralPosition.exists_lipschitz_vector_approximation line 66
6. lemma OAI.UniversalFInfinity.GeneralPosition.exists_missing_point line 88
7. lemma OAI.UniversalFInfinity.GeneralPosition.exists_nonzero_approximation line 97
8. def OAI.UniversalFInfinity.GeneralPosition.cutoff line 121
9. lemma OAI.UniversalFInfinity.GeneralPosition.cutoff_nonneg line 122
10. lemma OAI.UniversalFInfinity.GeneralPosition.cutoff_le_one line 123
11. lemma OAI.UniversalFInfinity.GeneralPosition.cutoff_small line 124
12. lemma OAI.UniversalFInfinity.GeneralPosition.cutoff_large line 129
13. lemma OAI.UniversalFInfinity.GeneralPosition.continuous_cutoff line 132
14. lemma OAI.UniversalFInfinity.GeneralPosition.exists_relative_nonzero_approximation line 135
15. lemma OAI.UniversalFInfinity.GeneralPosition.relative_interpolation_bound line 163
16. abbrev OAI.UniversalFInfinity.Cellular.ChartDisk line 187
17. abbrev OAI.UniversalFInfinity.Cellular.ChartCore line 188
18. def OAI.UniversalFInfinity.Cellular.chartCoreInclusion line 190
19. def OAI.UniversalFInfinity.Cellular.chartCore line 194
20. lemma OAI.UniversalFInfinity.Cellular.chartCore_closedEmbedding line 196
21. def OAI.UniversalFInfinity.Cellular.chartDomain line 205
22. lemma OAI.UniversalFInfinity.Cellular.chartDomain_closed line 207
23. def OAI.UniversalFInfinity.Cellular.coreCoordinate line 210
24. lemma OAI.UniversalFInfinity.Cellular.coreCoordinate_fac line 216
25. lemma OAI.UniversalFInfinity.Cellular.coreCoordinate_frontier line 220
26. lemma OAI.UniversalFInfinity.Cellular.chartDomain_dimH_le line 239
27. def OAI.UniversalFInfinity.Cellular.chartCenter line 252
28. lemma OAI.UniversalFInfinity.Cellular.exists_chart_avoidance line 254
29. lemma OAI.UniversalFInfinity.Cellular.homotopy_trans_pointwise line 345
30. lemma OAI.UniversalFInfinity.Cellular.chartCenter_mem_range line 361
31. lemma OAI.UniversalFInfinity.Cellular.exists_finite_chart_avoidance line 364
32. lemma OAI.UniversalFInfinity.Cellular.exists_all_chart_avoidance line 415
33. def OAI.UniversalFInfinity.Attachment.chart line 446
34. lemma OAI.UniversalFInfinity.Attachment.exists_deformation_into_base line 449