OAI/GroupTheory/UniversalGroup/ControlledHomotopies.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.Milnor.diagramValue_one line 24
  2. theorem OAI.UniversalFInfinity.Milnor.diagram_uniform_homotopy_killing line 40
  3. def OAI.UniversalFInfinity.Cellular.KillsSpheres line 53
  4. lemma OAI.UniversalFInfinity.Cellular.cylinder_filling_after line 56
  5. structure OAI.UniversalFInfinity.Cellular.PartialHomotopy line 102
  6. def OAI.UniversalFInfinity.Cellular.PartialHomotopy.onSphere line 111
  7. def OAI.UniversalFInfinity.Cellular.PartialHomotopy.endpoints line 117
  8. lemma OAI.UniversalFInfinity.Cellular.PartialHomotopy.endpoints_compatible line 122
  9. lemma OAI.UniversalFInfinity.Cellular.PartialHomotopy.cell_extension_after line 127
  10. def OAI.UniversalFInfinity.Cellular.PartialHomotopy.next line 138
  11. def OAI.UniversalFInfinity.Cellular.PartialHomotopy.start line 168
  12. def OAI.UniversalFInfinity.Cellular.PartialHomotopy.toHomotopy line 178