OAI/GroupTheory/UniversalGroup/MilnorControl.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.Milnor.boundedInclusion line 19
  2. def OAI.UniversalFInfinity.Milnor.boundedContraction line 23
  3. lemma OAI.UniversalFInfinity.Milnor.compactMap_bounded line 30
  4. lemma OAI.UniversalFInfinity.Milnor.compactMap_nullhomotopic line 43
  5. lemma OAI.UniversalFInfinity.Milnor.sphereFillable line 48
  6. lemma OAI.UniversalFInfinity.Milnor.contractible line 65
  7. def OAI.UniversalFInfinity.Milnor.translate line 79
  8. lemma OAI.UniversalFInfinity.Milnor.translate_one line 81
  9. lemma OAI.UniversalFInfinity.Milnor.translate_mul line 83
  10. lemma OAI.UniversalFInfinity.Milnor.translate_mono line 85
  11. lemma OAI.UniversalFInfinity.Milnor.translate_valid line 87
  12. def OAI.UniversalFInfinity.Milnor.orbitSpan line 90
  13. lemma OAI.UniversalFInfinity.Milnor.orbitSpan_le line 99
  14. lemma OAI.UniversalFInfinity.Milnor.orbitSpan_mono line 100
  15. lemma OAI.UniversalFInfinity.Milnor.orbitSpan_contains line 104
  16. lemma OAI.UniversalFInfinity.Milnor.orbitSpan_invariant line 108
  17. lemma OAI.UniversalFInfinity.Milnor.orbitSpan_bounded line 113
  18. def OAI.UniversalFInfinity.Milnor.Controlled line 123
  19. lemma OAI.UniversalFInfinity.Milnor.controlled_orbitSpan line 126
  20. lemma OAI.UniversalFInfinity.Milnor.controlled_bounded line 127
  21. lemma OAI.UniversalFInfinity.Milnor.orbitSpan_finite_representatives line 132
  22. def OAI.UniversalFInfinity.Milnor.vertexMap line 151
  23. def OAI.UniversalFInfinity.Milnor.faceImage line 152
  24. def OAI.UniversalFInfinity.Milnor.imageShapes line 153
  25. lemma OAI.UniversalFInfinity.Milnor.faceImage_translate line 155
  26. lemma OAI.UniversalFInfinity.Milnor.faceImage_valid line 159
  27. lemma OAI.UniversalFInfinity.Milnor.faceImage_controlled line 163
  28. lemma OAI.UniversalFInfinity.Milnor.unionFace_valid line 172
  29. def OAI.UniversalFInfinity.Milnor.unionShapes line 197
  30. lemma OAI.UniversalFInfinity.Milnor.translate_union line 200
  31. lemma OAI.UniversalFInfinity.Milnor.unionFace_controlled line 203
  32. def OAI.UniversalFInfinity.Milnor.fresh line 214
  33. lemma OAI.UniversalFInfinity.Milnor.fresh_zero line 215
  34. lemma OAI.UniversalFInfinity.Milnor.fresh_injective line 216
  35. lemma OAI.UniversalFInfinity.Milnor.fresh_cross line 225
  36. def OAI.UniversalFInfinity.Milnor.shapeBound line 240
  37. lemma OAI.UniversalFInfinity.Milnor.orbit_below_bound line 242
  38. def OAI.UniversalFInfinity.Milnor.relayerFresh line 250
  39. def OAI.UniversalFInfinity.Milnor.relayerTarget line 252
  40. lemma OAI.UniversalFInfinity.Milnor.relayerLeftValid line 255
  41. lemma OAI.UniversalFInfinity.Milnor.relayerRightValid line 263
  42. lemma OAI.UniversalFInfinity.Milnor.relayerLeftMapValid line 274
  43. lemma OAI.UniversalFInfinity.Milnor.relayerRightMapValid line 279
  44. lemma OAI.UniversalFInfinity.Milnor.relayerFreshMapValid line 284
  45. def OAI.UniversalFInfinity.Milnor.relayerLeftMap line 289
  46. def OAI.UniversalFInfinity.Milnor.relayerRightMap line 291
  47. def OAI.UniversalFInfinity.Milnor.relayerFreshMap line 293
  48. def OAI.UniversalFInfinity.Milnor.relayerLeftHomotopy line 296
  49. def OAI.UniversalFInfinity.Milnor.relayerRightHomotopy line 298
  50. def OAI.UniversalFInfinity.Milnor.relayerHomotopy line 301
  51. lemma OAI.UniversalFInfinity.Milnor.relayerLeftPure line 304
  52. lemma OAI.UniversalFInfinity.Milnor.relayerRightPure line 311
  53. lemma OAI.UniversalFInfinity.Milnor.relayerLeftHomotopy_fixed line 319
  54. lemma OAI.UniversalFInfinity.Milnor.relayerRightHomotopy_fixed line 324
  55. theorem OAI.UniversalFInfinity.Milnor.relayerHomotopy_fixed line 330