OAI/CategoryTheory/Thomason/CylinderInterchange.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Cylinder Interchange.

  1. lemma OAI.Thomason.GrayRecursive.tensorFace_tensorFace line 15
  2. lemma OAI.Thomason.GrayRecursive.restrictCylinder_restrict line 23
  3. lemma OAI.Thomason.GrayRecursive.FaceMatching.restrict line 30
  4. lemma OAI.Thomason.GrayRecursive.FaceMatching.paste_left line 40
  5. lemma OAI.Thomason.GrayRecursive.FaceMatching.paste_right line 48
  6. lemma OAI.Thomason.GrayRecursive.tensorFace_project line 56
  7. lemma OAI.Thomason.GrayRecursive.pasteCylinder_upper_face line 60
  8. lemma OAI.Thomason.GrayRecursive.intervalLabel_natural line 162
  9. lemma OAI.Thomason.GrayRecursive.tensorFace_zero_up line 167
  10. def OAI.Thomason.GrayRecursive.faceIdentityCylinder line 176
  11. lemma OAI.Thomason.GrayRecursive.faceIdentityCylinder_endpoint_top line 180
  12. lemma OAI.Thomason.GrayRecursive.faceIdentityCylinder_succ_edge line 191
  13. lemma OAI.Thomason.GrayRecursive.faceIdentityCylinder_succ_up line 197
  14. lemma OAI.Thomason.GrayRecursive.faceIdentityCylinder_zero_edge line 205
  15. lemma OAI.Thomason.GrayRecursive.faceIdentityCylinder_zero_up line 213
  16. lemma OAI.Thomason.GrayRecursive.faceIdentityCylinder_zero_endpoint line 220
  17. lemma OAI.Thomason.GrayRecursive.faceIdentityCylinder_left_matching line 227
  18. lemma OAI.Thomason.GrayRecursive.faceIdentityCylinder_right_matching line 236
  19. lemma OAI.Thomason.GrayRecursive.pasteCylinder_left_unit line 256
  20. lemma OAI.Thomason.GrayRecursive.pasteCylinder_right_unit line 324
  21. lemma OAI.Thomason.GrayRecursive.FaceMatching.pair line 402
  22. lemma OAI.Thomason.GrayRecursive.pasteCylinder_pair line 413
  23. lemma OAI.Thomason.GrayRecursive.FaceMatching.homCompose line 429
  24. lemma OAI.Thomason.GrayRecursive.pasteCylinder_homCompose line 440
  25. lemma OAI.Thomason.GrayRecursive.FaceMatching.constantAt line 463
  26. lemma OAI.Thomason.GrayRecursive.pasteCylinder_constantAt line 468
  27. lemma OAI.Thomason.GrayRecursive.pasteCylinder_homCompose_left line 476
  28. lemma OAI.Thomason.GrayRecursive.pasteCylinder_homCompose_right line 489
  29. lemma OAI.Thomason.GrayRecursive.FaceMatching.concat line 502
  30. lemma OAI.Thomason.GrayRecursive.IntervalMatching.paste line 515
  31. lemma OAI.Thomason.GrayRecursive.IntervalMatching.homCompose line 538
  32. lemma OAI.Thomason.GrayRecursive.concatInterval_shuffle_left line 548
  33. lemma OAI.Thomason.GrayRecursive.concatInterval_shuffle_right line 557
  34. lemma OAI.Thomason.GrayRecursive.concatInterval_four line 566
  35. lemma OAI.Thomason.GrayRecursive.IntervalMatching.of_val line 576