OAI/GroupTheory/FiniteType/SimplexHomotopy.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimplexHomotopy.diskMap line 24
  2. def OAI.SimplexHomotopy.sideMap line 27
  3. lemma OAI.SimplexHomotopy.boundary_compat line 31
  4. lemma OAI.SimplexHomotopy.boundary_compat_forward line 35
  5. lemma OAI.SimplexHomotopy.sideMap_time line 38
  6. theorem OAI.SimplexHomotopy.exists_extension line 42
  7. theorem OAI.SimplexHomotopy.exists_disk_cylinder line 61
  8. theorem OAI.SimplexHomotopy.exists_prescribed line 88
  9. lemma OAI.SimplexBoundary.face_injective line 121
  10. lemma OAI.SimplexBoundary.face_face line 128
  11. instance OAI.SimplexBoundary.boundary_zero_isEmpty line 137
  12. theorem OAI.SimplexBoundary.face_overlap line 147
  13. theorem OAI.SimplexBoundary.compatible_faces line 170
  14. def OAI.SimplexBoundary.glueHomotopies line 196
  15. theorem OAI.SimplexBoundary.glueHomotopies_face line 207
  16. structure OAI.SingularTightening.System line 225
  17. def OAI.SingularTightening.topMap line 235
  18. lemma OAI.SingularTightening.boundary_compatible line 238
  19. def OAI.SingularTightening.boundaryHom line 254
  20. lemma OAI.SingularTightening.boundaryHom_zero line 259
  21. lemma OAI.SingularTightening.boundaryHom_one line 265
  22. theorem OAI.SingularTightening.exists_next line 270
  23. def OAI.SingularTightening.next line 283
  24. lemma OAI.SingularTightening.next_zero line 287
  25. lemma OAI.SingularTightening.next_face line 291
  26. lemma OAI.SingularTightening.next_top line 300
  27. def OAI.SingularTightening.extendHom line 304
  28. lemma OAI.SingularTightening.extendHom_old line 312
  29. lemma OAI.SingularTightening.extendHom_new line 317
  30. def OAI.SingularTightening.extend line 321
  31. theorem OAI.SingularTightening.exists_baseHom line 349
  32. def OAI.SingularTightening.baseHom line 360
  33. def OAI.SingularTightening.base line 364
  34. def OAI.SingularTightening.system line 378
  35. def OAI.SingularTightening.hom line 383
  36. lemma OAI.SingularTightening.hom_zero line 387
  37. lemma OAI.SingularTightening.hom_top line 391
  38. lemma OAI.SingularTightening.hom_face line 395