OAI/GroupTheory/UniversalGroup/CoveringAttachments.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.Milnor.group_compactFundamentalSet line 17
  2. lemma OAI.UniversalFInfinity.Milnor.graph_compactFundamentalSet line 22
  3. lemma OAI.UniversalFInfinity.Milnor.presentation_compactFundamentalSet line 26
  4. lemma OAI.UniversalFInfinity.Milnor.presentation_equivariant_map line 32
  5. lemma OAI.UniversalFInfinity.Milnor.exists_stage_section line 45
  6. def OAI.UniversalFInfinity.Attachment.cellCenter line 65
  7. def OAI.UniversalFInfinity.Attachment.punctured line 66
  8. def OAI.UniversalFInfinity.Attachment.rawCoordinate line 68
  9. lemma OAI.UniversalFInfinity.Attachment.base_mem_punctured line 71
  10. lemma OAI.UniversalFInfinity.Attachment.cell_mem_punctured line 75
  11. lemma OAI.UniversalFInfinity.Attachment.punctured_open line 98
  12. lemma OAI.UniversalFInfinity.Attachment.continuous_punctured line 116
  13. abbrev OAI.UniversalFInfinity.Attachment.PuncturedDisk line 158
  14. def OAI.UniversalFInfinity.Attachment.puncturedBoundary line 160
  15. def OAI.UniversalFInfinity.Attachment.puncturedCell line 169
  16. def OAI.UniversalFInfinity.Attachment.puncturedBase line 172
  17. lemma OAI.UniversalFInfinity.Attachment.puncturedCell_boundary line 174
  18. def OAI.UniversalFInfinity.Attachment.puncturedLift line 178
  19. lemma OAI.UniversalFInfinity.Attachment.puncturedLift_base line 209
  20. lemma OAI.UniversalFInfinity.Attachment.puncturedLift_cell line 214
  21. lemma OAI.UniversalFInfinity.Attachment.punctured_surjective line 233
  22. def OAI.UniversalFInfinity.Attachment.radialSphere line 242
  23. lemma OAI.UniversalFInfinity.Attachment.radialSphere_boundary line 251
  24. def OAI.UniversalFInfinity.Attachment.radialDisk line 257
  25. lemma OAI.UniversalFInfinity.Attachment.radialDisk_zero line 271
  26. lemma OAI.UniversalFInfinity.Attachment.radialDisk_one line 274
  27. lemma OAI.UniversalFInfinity.Attachment.radialDisk_boundary line 277
  28. def OAI.UniversalFInfinity.Attachment.radialRetraction line 284
  29. lemma OAI.UniversalFInfinity.Attachment.radialRetraction_base line 288
  30. lemma OAI.UniversalFInfinity.Attachment.radialRetraction_cell line 289
  31. def OAI.UniversalFInfinity.Attachment.radialPaths line 293
  32. lemma OAI.UniversalFInfinity.Attachment.radialPaths_base line 303
  33. lemma OAI.UniversalFInfinity.Attachment.radialPaths_cell line 305
  34. def OAI.UniversalFInfinity.Attachment.puncturedInclusion line 311
  35. def OAI.UniversalFInfinity.Attachment.radialEnd line 312
  36. def OAI.UniversalFInfinity.Attachment.radialHomotopy line 314
  37. lemma OAI.UniversalFInfinity.Attachment.radialHomotopy_base line 329
  38. lemma OAI.UniversalFInfinity.Attachment.cell_eq_openCell_iff line 332
  39. lemma OAI.UniversalFInfinity.Attachment.openCell_disjoint line 355
  40. lemma OAI.UniversalFInfinity.Attachment.openCell_selection_closed line 361
  41. lemma OAI.UniversalFInfinity.Attachment.compact_finitely_many_openCells line 384
  42. def OAI.UniversalFInfinity.Cellular.patchFun line 415
  43. lemma OAI.UniversalFInfinity.Cellular.patchFun_on line 419
  44. lemma OAI.UniversalFInfinity.Cellular.patchFun_off line 422
  45. lemma OAI.UniversalFInfinity.Cellular.continuous_patchFun line 425
  46. def OAI.UniversalFInfinity.Cellular.patch line 445
  47. lemma OAI.UniversalFInfinity.Cellular.patch_on line 449
  48. lemma OAI.UniversalFInfinity.Cellular.patch_off line 453
  49. def OAI.UniversalFInfinity.Cellular.patchHomotopy line 457