OAI/GroupTheory/UniversalGroup/GeneralPosition.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.GeneralPosition.lipschitz_insertNth line 17
  2. lemma OAI.UniversalFInfinity.GeneralPosition.sphere_subset_faces line 29
  3. lemma OAI.UniversalFInfinity.GeneralPosition.dimH_cube_boundary_le line 45
  4. lemma OAI.UniversalFInfinity.GeneralPosition.dimH_cube_boundary_subtype_le line 58
  5. lemma OAI.UniversalFInfinity.Attachment.sphere_filling_preserved line 72
  6. lemma OAI.UniversalFInfinity.Attachment.dimH_disk_subtype_le line 85
  7. lemma OAI.UniversalFInfinity.Attachment.filling_reflected line 90
  8. lemma OAI.UniversalFInfinity.Attachment.pathConnectedSpace line 108
  9. instance OAI.UniversalFInfinity.Cayley.presentationCoverT2 line 132
  10. instance OAI.UniversalFInfinity.Cayley.presentationCoverCW line 135
  11. lemma OAI.UniversalFInfinity.Cayley.presentationCover_pathConnected line 139
  12. lemma OAI.UniversalFInfinity.Cayley.presentationCover_sphereFill line 148
  13. lemma OAI.UniversalFInfinity.Cayley.presentationCover_simplyConnected line 158
  14. abbrev OAI.UniversalFInfinity.Orbits line 172
  15. lemma OAI.UniversalFInfinity.orbit_mk_smul line 174
  16. lemma OAI.UniversalFInfinity.orbit_out_translate line 178
  17. lemma OAI.UniversalFInfinity.orbitCoordinates_bijective line 187
  18. def OAI.UniversalFInfinity.orbitCoordinates line 203
  19. lemma OAI.UniversalFInfinity.orbitCoordinates_apply line 206
  20. def OAI.UniversalFInfinity.Cellular.actionChart line 219
  21. lemma OAI.UniversalFInfinity.Cellular.actionChart_apply line 222
  22. lemma OAI.UniversalFInfinity.Cellular.actionChart_image line 225
  23. lemma OAI.UniversalFInfinity.Cellular.actionChart_source line 229
  24. lemma OAI.UniversalFInfinity.Cellular.actionChart_continuousOn line 233
  25. lemma OAI.UniversalFInfinity.Cellular.actionChart_continuousOn_symm line 237
  26. lemma OAI.UniversalFInfinity.Cellular.actionChart_open line 251
  27. lemma OAI.UniversalFInfinity.Cellular.actionChart_closed line 257
  28. lemma OAI.UniversalFInfinity.Cellular.closedCell_smul line 264
  29. def OAI.UniversalFInfinity.Cellular.actionCW line 273
  30. lemma OAI.UniversalFInfinity.Cellular.actionChart_smul line 330
  31. lemma OAI.UniversalFInfinity.Milnor.vertexTranslate_injective line 341
  32. lemma OAI.UniversalFInfinity.Milnor.translate_card line 348
  33. abbrev OAI.UniversalFInfinity.Milnor.StageCell line 351
  34. def OAI.UniversalFInfinity.Milnor.cellTranslate line 353
  35. instance OAI.UniversalFInfinity.Milnor.cellAction line 356
  36. lemma OAI.UniversalFInfinity.Milnor.cell_smul_val line 361
  37. lemma OAI.UniversalFInfinity.Milnor.cellAction_free line 364
  38. abbrev OAI.UniversalFInfinity.Milnor.CellOrbits line 373
  39. def OAI.UniversalFInfinity.Milnor.cellCoordinates line 375
  40. lemma OAI.UniversalFInfinity.Milnor.cellCoordinates_apply line 378
  41. instance OAI.UniversalFInfinity.Milnor.cellOrbits_finite line 381
  42. lemma OAI.UniversalFInfinity.Milnor.stage_smul_support line 400
  43. lemma OAI.UniversalFInfinity.Milnor.stage_openCell line 404
  44. lemma OAI.UniversalFInfinity.Milnor.stage_closedCell line 408
  45. lemma OAI.UniversalFInfinity.Milnor.stage_openCell_smul line 413
  46. lemma OAI.UniversalFInfinity.Milnor.stage_closedCell_smul line 427
  47. def OAI.UniversalFInfinity.Milnor.stageEquivariantCW line 444