OAI/GroupTheory/UniversalGroup/CellularLifting.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.Cellular.Disk line 12
  2. abbrev OAI.UniversalFInfinity.Cellular.Sphere line 13
  3. def OAI.UniversalFInfinity.Cellular.boundary line 15
  4. lemma OAI.UniversalFInfinity.Cellular.continuous_boundary line 18
  5. def OAI.UniversalFInfinity.Cellular.characteristic line 24
  6. lemma OAI.UniversalFInfinity.Cellular.range_characteristic line 28
  7. lemma OAI.UniversalFInfinity.Cellular.continuousOn_iff_characteristic line 35
  8. abbrev OAI.UniversalFInfinity.Cellular.Skeleton line 63
  9. lemma OAI.UniversalFInfinity.Cellular.skeleton_mono line 66
  10. lemma OAI.UniversalFInfinity.Cellular.sphere_mem_skeleton line 70
  11. lemma OAI.UniversalFInfinity.Cellular.characteristic_mem_skeleton line 74
  12. lemma OAI.UniversalFInfinity.Cellular.openCell_not_skeleton line 80
  13. structure OAI.UniversalFInfinity.Cellular.PartialLift line 84
  14. def OAI.UniversalFInfinity.Cellular.DiskRLP line 90
  15. def OAI.UniversalFInfinity.Cellular.attachValue line 99
  16. lemma OAI.UniversalFInfinity.Cellular.attachValue_old line 109
  17. lemma OAI.UniversalFInfinity.Cellular.attachValue_interior line 114
  18. lemma OAI.UniversalFInfinity.Cellular.attachValue_characteristic line 141
  19. lemma OAI.UniversalFInfinity.Cellular.attachValue_continuous line 154
  20. def OAI.UniversalFInfinity.Cellular.PartialLift.onSphere line 187
  21. lemma OAI.UniversalFInfinity.Cellular.PartialLift.exists_cell_extension line 194
  22. def OAI.UniversalFInfinity.Cellular.PartialLift.next line 203
  23. lemma OAI.UniversalFInfinity.Cellular.PartialLift.next_eq line 221
  24. def OAI.UniversalFInfinity.Cellular.PartialLift.zero line 226
  25. def OAI.UniversalFInfinity.Cellular.stages line 239
  26. lemma OAI.UniversalFInfinity.Cellular.stages_agree line 243
  27. lemma OAI.UniversalFInfinity.Cellular.exists_skeleton line 250
  28. def OAI.UniversalFInfinity.Cellular.liftValue line 254
  29. lemma OAI.UniversalFInfinity.Cellular.liftValue_eq line 259
  30. lemma OAI.UniversalFInfinity.Cellular.continuousOn_liftValue line 269
  31. lemma OAI.UniversalFInfinity.Cellular.liftValue_fac line 280
  32. theorem OAI.UniversalFInfinity.Cellular.exists_lift line 287
  33. def OAI.UniversalFInfinity.Cellular.SphereFillable line 298
  34. lemma OAI.UniversalFInfinity.Cellular.disk_coord line 301
  35. lemma OAI.UniversalFInfinity.Cellular.disk_mem line 305
  36. def OAI.UniversalFInfinity.Cellular.diskCons line 310
  37. lemma OAI.UniversalFInfinity.Cellular.continuous_diskCons line 318
  38. def OAI.UniversalFInfinity.Cellular.diskTail line 329
  39. lemma OAI.UniversalFInfinity.Cellular.continuous_diskTail line 332
  40. def OAI.UniversalFInfinity.Cellular.diskTime line 336
  41. lemma OAI.UniversalFInfinity.Cellular.continuous_diskTime line 339
  42. lemma OAI.UniversalFInfinity.Cellular.diskTail_cons line 342
  43. lemma OAI.UniversalFInfinity.Cellular.diskTime_cons line 347
  44. lemma OAI.UniversalFInfinity.Cellular.sphere_iff_coord line 353
  45. lemma OAI.UniversalFInfinity.Cellular.cons_mem_sphere_of_boundary line 359
  46. lemma OAI.UniversalFInfinity.Cellular.cons_zero_mem_sphere line 364
  47. lemma OAI.UniversalFInfinity.Cellular.cons_one_mem_sphere line 369
  48. lemma OAI.UniversalFInfinity.Cellular.sphere_split line 374
  49. lemma OAI.UniversalFInfinity.Cellular.continuous_liftCover line 384
  50. def OAI.UniversalFInfinity.Cellular.cylinderFace line 395
  51. lemma OAI.UniversalFInfinity.Cellular.cylinderFace_closed line 400
  52. lemma OAI.UniversalFInfinity.Cellular.cylinderFace_cover line 409
  53. def OAI.UniversalFInfinity.Cellular.pathEndpoint line 419
  54. def OAI.UniversalFInfinity.Cellular.faceTail line 425
  55. def OAI.UniversalFInfinity.Cellular.faceSphere line 429
  56. def OAI.UniversalFInfinity.Cellular.faceTime line 432
  57. def OAI.UniversalFInfinity.Cellular.faceMap line 436
  58. lemma OAI.UniversalFInfinity.Cellular.faceTime_eq_zero line 444
  59. lemma OAI.UniversalFInfinity.Cellular.faceTime_eq_one line 451
  60. lemma OAI.UniversalFInfinity.Cellular.faceMap_compat line 461
  61. def OAI.UniversalFInfinity.Cellular.cylinderBoundaryMap line 494
  62. lemma OAI.UniversalFInfinity.Cellular.cylinderBoundaryMap_face line 499
  63. theorem OAI.UniversalFInfinity.Cellular.pathEndpoint_RLP line 507
  64. theorem OAI.UniversalFInfinity.Cellular.contractible_of_sphereFillable line 548