OAI/GroupTheory/UniversalGroup/TorusBundles.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.Milnor.map_smul line 21
  2. lemma OAI.UniversalFInfinity.Milnor.map_leftInverse line 29
  3. lemma OAI.UniversalFInfinity.Milnor.map_closedEmbedding line 37
  4. def OAI.UniversalFInfinity.Milnor.smulMap line 43
  5. lemma OAI.UniversalFInfinity.Milnor.smulMap_closedEmbedding line 44
  6. instance OAI.UniversalFInfinity.TorusGeometry.cosetTopology line 53
  7. instance OAI.UniversalFInfinity.TorusGeometry.(instance at line 54) line 54
  8. def OAI.UniversalFInfinity.TorusGeometry.transition line 56
  9. lemma OAI.UniversalFInfinity.TorusGeometry.transition_apply line 58
  10. lemma OAI.UniversalFInfinity.TorusGeometry.transition_embedding line 60
  11. abbrev OAI.UniversalFInfinity.TorusGeometry.Space line 64
  12. def OAI.UniversalFInfinity.TorusGeometry.vertex line 65
  13. def OAI.UniversalFInfinity.TorusGeometry.coordinateAction line 67
  14. lemma OAI.UniversalFInfinity.TorusGeometry.coordinateAction_compatible line 69
  15. lemma OAI.UniversalFInfinity.TorusGeometry.coordinateAction_one line 85
  16. lemma OAI.UniversalFInfinity.TorusGeometry.coordinateAction_mul line 89
  17. def OAI.UniversalFInfinity.TorusGeometry.action line 95
  18. instance OAI.UniversalFInfinity.TorusGeometry.action_continuous line 102
  19. lemma OAI.UniversalFInfinity.TorusGeometry.smul_vertex line 105
  20. lemma OAI.UniversalFInfinity.TorusGeometry.smul_edge line 107
  21. def OAI.UniversalFInfinity.GraphBundle.inclusionFun line 127
  22. lemma OAI.UniversalFInfinity.GraphBundle.inclusionFun_vertex line 130
  23. lemma OAI.UniversalFInfinity.GraphBundle.inclusionFun_interior line 133
  24. lemma OAI.UniversalFInfinity.GraphBundle.inclusionFun_edge line 137
  25. def OAI.UniversalFInfinity.GraphBundle.inclusion line 150
  26. lemma OAI.UniversalFInfinity.GraphBundle.inclusion_vertex line 157
  27. lemma OAI.UniversalFInfinity.GraphBundle.inclusion_interior line 159
  28. lemma OAI.UniversalFInfinity.GraphBundle.inclusion_edge line 161
  29. lemma OAI.UniversalFInfinity.GraphBundle.inclusion_injective line 165
  30. lemma OAI.UniversalFInfinity.GraphBundle.inclusion_vertex_preimage line 169
  31. lemma OAI.UniversalFInfinity.GraphBundle.inclusion_edge_preimage line 184
  32. lemma OAI.UniversalFInfinity.GraphBundle.inclusion_closedEmbedding line 233
  33. theorem OAI.UniversalFInfinity.GraphBundle.compact_coordinates line 255
  34. def OAI.UniversalFInfinity.TorusGeometry.vertexShapes line 291
  35. lemma OAI.UniversalFInfinity.TorusGeometry.vertexShapes_left line 292
  36. lemma OAI.UniversalFInfinity.TorusGeometry.vertexShapes_map line 293
  37. def OAI.UniversalFInfinity.TorusGeometry.stageForward line 299
  38. lemma OAI.UniversalFInfinity.TorusGeometry.stageForward_full line 301
  39. def OAI.UniversalFInfinity.TorusGeometry.left line 305
  40. def OAI.UniversalFInfinity.TorusGeometry.right line 307
  41. lemma OAI.UniversalFInfinity.TorusGeometry.left_full line 309
  42. lemma OAI.UniversalFInfinity.TorusGeometry.right_full line 311
  43. abbrev OAI.UniversalFInfinity.TorusGeometry.Stage line 314
  44. def OAI.UniversalFInfinity.TorusGeometry.stageFull line 315
  45. lemma OAI.UniversalFInfinity.TorusGeometry.stageFull_closedEmbedding line 319
  46. lemma OAI.UniversalFInfinity.TorusGeometry.stageFull_vertex line 322
  47. lemma OAI.UniversalFInfinity.TorusGeometry.stageFull_interior line 324
  48. lemma OAI.UniversalFInfinity.TorusGeometry.stageFull_edge line 326
  49. lemma OAI.UniversalFInfinity.TorusGeometry.next_ne line 330
  50. theorem OAI.UniversalFInfinity.TorusGeometry.compact_controlled line 336
  51. lemma OAI.UniversalFInfinity.TorusGeometry.stage_range_smul line 367
  52. lemma OAI.UniversalFInfinity.TorusGeometry.compact_orbit_controlled line 390
  53. lemma OAI.UniversalFInfinity.TorusGeometry.equivariant_controlled line 399
  54. def OAI.UniversalFInfinity.TorusGeometry.factorStage line 411
  55. lemma OAI.UniversalFInfinity.TorusGeometry.factorStage_spec line 419