OAI/GroupTheory/UniversalGroup/TorusHomotopies.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.TorusGeometry.idx line 25
  2. lemma OAI.UniversalFInfinity.TorusGeometry.idx_next line 26
  3. lemma OAI.UniversalFInfinity.TorusGeometry.left_full_eq line 29
  4. def OAI.UniversalFInfinity.TorusGeometry.firstH line 38
  5. lemma OAI.UniversalFInfinity.TorusGeometry.firstH_zero line 41
  6. lemma OAI.UniversalFInfinity.TorusGeometry.firstH_one line 46
  7. def OAI.UniversalFInfinity.TorusGeometry.squareLeft line 51
  8. def OAI.UniversalFInfinity.TorusGeometry.squareRight line 54
  9. lemma OAI.UniversalFInfinity.TorusGeometry.square_start line 58
  10. lemma OAI.UniversalFInfinity.TorusGeometry.squareLeft_one line 65
  11. lemma OAI.UniversalFInfinity.TorusGeometry.squareRight_one line 68
  12. def OAI.UniversalFInfinity.TorusGeometry.secondH line 78
  13. lemma OAI.UniversalFInfinity.TorusGeometry.secondH_full line 82
  14. lemma OAI.UniversalFInfinity.TorusGeometry.secondH_one line 88
  15. lemma OAI.UniversalFInfinity.TorusGeometry.secondH_start_natural line 94
  16. lemma OAI.UniversalFInfinity.TorusGeometry.twoGhost_square line 103
  17. def OAI.UniversalFInfinity.TorusGeometry.finalIndex line 115
  18. lemma OAI.UniversalFInfinity.TorusGeometry.finalIndex_next line 116
  19. def OAI.UniversalFInfinity.TorusGeometry.finalLower line 119
  20. def OAI.UniversalFInfinity.TorusGeometry.finalUpper line 121
  21. def OAI.UniversalFInfinity.TorusGeometry.finalHigh line 124
  22. lemma OAI.UniversalFInfinity.TorusGeometry.final_natural line 128
  23. def OAI.UniversalFInfinity.TorusGeometry.finalPoint line 136
  24. def OAI.UniversalFInfinity.TorusGeometry.shifted_stage line 139
  25. lemma OAI.UniversalFInfinity.TorusGeometry.shifted_stage_vertex line 161
  26. lemma OAI.UniversalFInfinity.TorusGeometry.shifted_stage_edge line 164
  27. theorem OAI.UniversalFInfinity.TorusGeometry.shifted_stage_nullhomotopic line 172
  28. lemma OAI.UniversalFInfinity.TorusGeometry.shifted_stage_full line 247
  29. lemma OAI.UniversalFInfinity.PathFamilies.diagonalSquare_mem line 281
  30. lemma OAI.UniversalFInfinity.TorusGeometry.vertexShapes_mono line 297
  31. lemma OAI.UniversalFInfinity.TorusGeometry.stage_range_mono line 300
  32. def OAI.UniversalFInfinity.TorusGeometry.stageInclusion line 310
  33. lemma OAI.UniversalFInfinity.TorusGeometry.stageInclusion_full line 312
  34. lemma OAI.UniversalFInfinity.TorusGeometry.edge_mem_stage line 315
  35. lemma OAI.UniversalFInfinity.TorusGeometry.shiftHomotopy_controlled line 319
  36. lemma OAI.UniversalFInfinity.TorusGeometry.shiftIterateHomotopy_controlled line 336
  37. def OAI.UniversalFInfinity.TorusGeometry.homotopyFactor line 365
  38. lemma OAI.UniversalFInfinity.TorusGeometry.doubleShiftHomotopy_controlled line 383
  39. theorem OAI.UniversalFInfinity.TorusGeometry.uniform_stage_nullhomotopy line 409