OAI/GroupTheory/UniversalGroup/SphereHomotopies.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.SphereCube.bottom_repr line 25
  2. lemma OAI.UniversalFInfinity.SphereCube.top_repr line 31
  3. lemma OAI.UniversalFInfinity.SphereCube.side_repr line 37
  4. def OAI.UniversalFInfinity.SphereCube.nullTopPaths line 48
  5. def OAI.UniversalFInfinity.SphereCube.nullSpherePaths line 51
  6. lemma OAI.UniversalFInfinity.SphereCube.nullSphere_zero line 62
  7. lemma OAI.UniversalFInfinity.SphereCube.nullSphere_one line 74
  8. def OAI.UniversalFInfinity.SphereCube.nullSphere line 81
  9. def OAI.UniversalFInfinity.SphereCube.basedDiskLoop line 95
  10. theorem OAI.UniversalFInfinity.SphereCube.killsSpheres_of_null_cubes line 100
  11. lemma OAI.UniversalFInfinity.SphereCube.killsSpheres_of_homotopy_zero line 136
  12. def OAI.UniversalFInfinity.Cellular.towerComposite line 153
  13. def OAI.UniversalFInfinity.Cellular.towerPartialHomotopy line 159
  14. def OAI.UniversalFInfinity.Cellular.towerHomotopy line 164
  15. lemma OAI.UniversalFInfinity.SphereCube.rim_nullhomotopy_of_joined line 177
  16. lemma OAI.UniversalFInfinity.SphereCube.fills_of_rim_nullhomotopy line 192
  17. lemma OAI.UniversalFInfinity.SphereCube.killsSpheres_of_connected_image line 223
  18. lemma OAI.UniversalFInfinity.Cellular.KillsSpheres.post line 241
  19. lemma OAI.UniversalFInfinity.Cellular.joined_of_killsSpheres_one line 246
  20. lemma OAI.UniversalFInfinity.Milnor.uniform_low_fp line 270
  21. def OAI.UniversalFInfinity.Milnor.Represents line 287
  22. lemma OAI.UniversalFInfinity.Milnor.uniform_diagram_sphere_ghost line 290
  23. lemma OAI.UniversalFInfinity.Milnor.stage_bounded_dimension line 343
  24. lemma OAI.UniversalFInfinity.Milnor.Represents.comp line 364
  25. lemma OAI.UniversalFInfinity.Milnor.Represents.id line 372
  26. def OAI.UniversalFInfinity.Milnor.iterateHom line 377
  27. def OAI.UniversalFInfinity.Milnor.ghostShapes line 382
  28. def OAI.UniversalFInfinity.Milnor.ghostMap line 386
  29. lemma OAI.UniversalFInfinity.Milnor.ghostMap_represents line 389
  30. lemma OAI.UniversalFInfinity.Milnor.ghostMap_kills line 392
  31. lemma OAI.UniversalFInfinity.Milnor.ghostComposite_represents line 395
  32. theorem OAI.UniversalFInfinity.Milnor.diagram_uniform_stage_nullhomotopy line 406