OAI/GroupTheory/UniversalGroup/TorusSpheres.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.Milnor.evenLayer line 23
  2. def OAI.UniversalFInfinity.Milnor.oddLayer line 24
  3. lemma OAI.UniversalFInfinity.Milnor.evenLayer_injective line 25
  4. lemma OAI.UniversalFInfinity.Milnor.oddLayer_injective line 26
  5. lemma OAI.UniversalFInfinity.Milnor.even_ne_odd line 27
  6. lemma OAI.UniversalFInfinity.Milnor.mixed_face line 29
  7. def OAI.UniversalFInfinity.Milnor.mixedHomotopy line 45
  8. def OAI.UniversalFInfinity.Milnor.bridge line 50
  9. lemma OAI.UniversalFInfinity.Milnor.map_natural line 54
  10. lemma OAI.UniversalFInfinity.Milnor.mixedHomotopy_natural line 61
  11. lemma OAI.UniversalFInfinity.Milnor.bridge_natural line 74
  12. def OAI.UniversalFInfinity.TorusGeometry.lowerLabel line 90
  13. def OAI.UniversalFInfinity.TorusGeometry.upperLabel line 91
  14. def OAI.UniversalFInfinity.TorusGeometry.vertexToMilnor line 93
  15. def OAI.UniversalFInfinity.TorusGeometry.edgeToMilnor line 96
  16. lemma OAI.UniversalFInfinity.TorusGeometry.edgeToMilnor_zero line 99
  17. lemma OAI.UniversalFInfinity.TorusGeometry.edgeToMilnor_one line 102
  18. def OAI.UniversalFInfinity.TorusGeometry.toMilnor line 112
  19. lemma OAI.UniversalFInfinity.TorusGeometry.toMilnor_vertex line 115
  20. lemma OAI.UniversalFInfinity.TorusGeometry.toMilnor_edge line 117
  21. lemma OAI.UniversalFInfinity.TorusGeometry.lowerLabel_action line 121
  22. lemma OAI.UniversalFInfinity.TorusGeometry.upperLabel_action line 125
  23. lemma OAI.UniversalFInfinity.TorusGeometry.toMilnor_equivariant line 134
  24. def OAI.UniversalFInfinity.GraphBundle.contractionSquare line 161
  25. lemma OAI.UniversalFInfinity.GraphBundle.contractionSquare_filling line 180
  26. theorem OAI.UniversalFInfinity.GraphBundle.homogeneous_contractible line 190
  27. lemma OAI.UniversalFInfinity.TorusGeometry.contractible line 238
  28. lemma OAI.UniversalFInfinity.Milnor.stageCell_dimension_bound line 250
  29. lemma OAI.UniversalFInfinity.Milnor.stageEquivariant_bounded line 258
  30. lemma OAI.UniversalFInfinity.Milnor.stage_compactFundamentalSet line 273
  31. lemma OAI.UniversalFInfinity.TorusGeometry.exists_moveOffset line 299
  32. lemma OAI.UniversalFInfinity.TorusGeometry.stage_compact_representatives line 315
  33. lemma OAI.UniversalFInfinity.TorusGeometry.toMilnor_controlled line 349
  34. lemma OAI.UniversalFInfinity.SphereTopology.sphereFillable_of_contractible line 363
  35. theorem OAI.UniversalFInfinity.TorusGeometry.milnor_uniform_nullhomotopy line 389
  36. lemma OAI.UniversalFInfinity.TorusGeometry.diagram_graph_uniform_nullhomotopy line 471
  37. theorem OAI.UniversalFInfinity.TorusGeometry.diagram_milnor_uniform_nullhomotopy line 485