OAI/GroupTheory/FiniteType/PresentationGeometryDescend.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PresentationGeometry.Adjunction.descend line 17
  2. theorem OAI.PresentationGeometry.Adjunction.descend_old line 34
  3. theorem OAI.PresentationGeometry.Adjunction.descend_disk line 39
  4. theorem OAI.PresentationGeometry.Adjunction.continuous_descend line 43
  5. def OAI.PresentationGeometry.Cells.innerClosed line 52
  6. def OAI.PresentationGeometry.Cells.collar line 56
  7. def OAI.PresentationGeometry.Cells.cellInterior line 59
  8. theorem OAI.PresentationGeometry.Cells.collar_isOpen line 66
  9. theorem OAI.PresentationGeometry.Cells.cellInterior_isOpen line 72
  10. theorem OAI.PresentationGeometry.Cells.mem_collar_old line 76
  11. theorem OAI.PresentationGeometry.Cells.mem_collar_disk_iff line 86
  12. theorem OAI.PresentationGeometry.Cells.characteristic_on_openDisk line 104
  13. theorem OAI.PresentationGeometry.Cells.cellInterior_pairwiseDisjoint line 109
  14. theorem OAI.PresentationGeometry.Cells.collar_union_interiors line 120
  15. theorem OAI.PresentationGeometry.Cells.cellInterior_contractible line 136
  16. theorem OAI.PresentationGeometry.Cells.annulus_pathConnected line 141
  17. theorem OAI.PresentationGeometry.Cells.collar_inter_interior line 169
  18. theorem OAI.PresentationGeometry.Cells.collar_inter_interior_pathConnected line 186
  19. theorem OAI.PresentationGeometry.Cells.collar_fundamentalGroupMap_surjective line 194
  20. abbrev OAI.PresentationGeometry.Cells.Shell line 213
  21. instance OAI.PresentationGeometry.Cells.shell_compactSpace line 215
  22. def OAI.PresentationGeometry.Cells.shellInDisk line 222
  23. theorem OAI.PresentationGeometry.Cells.shellInDisk_continuous line 225
  24. def OAI.PresentationGeometry.Cells.shellBoundary line 229
  25. theorem OAI.PresentationGeometry.Cells.shellBoundary_closed line 231
  26. def OAI.PresentationGeometry.Cells.shellAttach line 237
  27. abbrev OAI.PresentationGeometry.Cells.ClosedCollarSpace line 241
  28. instance OAI.PresentationGeometry.Cells.(instance at line 243) line 243
  29. def OAI.PresentationGeometry.Cells.shellInclude line 246
  30. theorem OAI.PresentationGeometry.Cells.shellInclude_old line 253
  31. theorem OAI.PresentationGeometry.Cells.shellInclude_disk line 257
  32. theorem OAI.PresentationGeometry.Cells.shellInclude_continuous line 262
  33. theorem OAI.PresentationGeometry.Cells.shellInclude_injective line 268
  34. theorem OAI.PresentationGeometry.Cells.shellInclude_isClosedEmbedding line 310
  35. theorem OAI.PresentationGeometry.Cells.collar_subset_range_shellInclude line 314
  36. def OAI.PresentationGeometry.Cells.collarToShell line 323
  37. theorem OAI.PresentationGeometry.Cells.shellInclude_collarToShell line 330
  38. theorem OAI.PresentationGeometry.Cells.shell_norm_pos line 341
  39. def OAI.PresentationGeometry.Cells.shellUnit line 344
  40. theorem OAI.PresentationGeometry.Cells.shellUnit_continuous line 351
  41. theorem OAI.PresentationGeometry.Cells.shellUnit_boundary line 358
  42. def OAI.PresentationGeometry.Cells.shellRetraction line 370
  43. theorem OAI.PresentationGeometry.Cells.shellRetraction_old line 377
  44. theorem OAI.PresentationGeometry.Cells.shellRetraction_disk line 381
  45. def OAI.PresentationGeometry.Cells.radialVector line 384
  46. theorem OAI.PresentationGeometry.Cells.norm_radialVector line 387
  47. def OAI.PresentationGeometry.Cells.radialDisk line 395
  48. theorem OAI.PresentationGeometry.Cells.radialDisk_continuous line 400
  49. theorem OAI.PresentationGeometry.Cells.radialDisk_zero line 409
  50. theorem OAI.PresentationGeometry.Cells.radialDisk_boundary line 413
  51. def OAI.PresentationGeometry.Cells.shellSlide line 419
  52. theorem OAI.PresentationGeometry.Cells.shellSlide_old line 427
  53. theorem OAI.PresentationGeometry.Cells.shellSlide_disk line 431
  54. theorem OAI.PresentationGeometry.Cells.shellSlide_continuous line 436
  55. theorem OAI.PresentationGeometry.Cells.shellSlide_zero line 451
  56. theorem OAI.PresentationGeometry.Cells.shellSlide_one line 459
  57. theorem OAI.PresentationGeometry.Cells.collarToShell_old line 474