OAI/CategoryTheory/Thomason/CylinderFaces.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Cylinder Faces.

  1. lemma OAI.Thomason.GrayRecursive.suspend_composable line 15
  2. lemma OAI.Thomason.GrayRecursive.suspend_comp line 20
  3. def OAI.Thomason.GrayRecursive.globeHom line 34
  4. def OAI.Thomason.GrayRecursive.globeHomMap line 41
  5. lemma OAI.Thomason.GrayRecursive.globe_horizontal_match line 47
  6. lemma OAI.Thomason.GrayRecursive.globe_horizontal_fixed line 54
  7. def OAI.Thomason.GrayRecursive.globeHorizontal line 64
  8. lemma OAI.Thomason.GrayRecursive.globeHorizontal_vertex line 70
  9. lemma OAI.Thomason.GrayRecursive.globeHorizontal_suspend line 84
  10. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.horizontal_seam line 114
  11. def OAI.Thomason.GrayRecursive.RectangleDiagram.horizontalDiagonalOne line 120
  12. def OAI.Thomason.GrayRecursive.RectangleDiagram.horizontalDiagonalTwo line 126
  13. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.horizontalDiagonalOne_map line 132
  14. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.horizontalDiagonalTwo_map line 135
  15. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.horizontalDiagonal_matching line 139
  16. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.horizontal_source_match line 146
  17. def OAI.Thomason.GrayRecursive.RectangleDiagram.horizontal line 154
  18. def OAI.Thomason.GrayRecursive.horizontalCylinder line 189
  19. lemma OAI.Thomason.GrayRecursive.globeHorizontal_natural line 206
  20. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.map_horizontalDiagonalOne line 225
  21. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.map_horizontalDiagonalTwo line 238
  22. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.horizontal_lift_map line 251
  23. lemma OAI.Thomason.GrayRecursive.horizontalCylinder_natural line 275
  24. lemma OAI.Thomason.GrayRecursive.project_up line 295
  25. lemma OAI.Thomason.GrayRecursive.project_zero_vertical line 313
  26. def OAI.Thomason.GrayRecursive.constantInterval line 317
  27. lemma OAI.Thomason.GrayRecursive.constantInterval_map line 322
  28. lemma OAI.Thomason.GrayRecursive.constantInterval_endpoint line 326
  29. lemma OAI.Thomason.GrayRecursive.constantInterval_edge line 331
  30. lemma OAI.Thomason.GrayRecursive.constantInterval_up line 336
  31. lemma OAI.Thomason.GrayRecursive.constantInterval_matching line 341
  32. lemma OAI.Thomason.GrayRecursive.constantInterval_ends line 347
  33. lemma OAI.Thomason.GrayRecursive.constantInterval_diagonal line 354
  34. lemma OAI.Thomason.GrayRecursive.constantInterval_concatDiagonalOne line 365
  35. lemma OAI.Thomason.GrayRecursive.constantInterval_concatDiagonalTwo line 385
  36. lemma OAI.Thomason.GrayRecursive.homCast_constantInterval line 405
  37. lemma OAI.Thomason.GrayRecursive.concatInterval_constant line 410
  38. def OAI.Thomason.GrayRecursive.globeHorizontalHom line 457
  39. lemma OAI.Thomason.GrayRecursive.constantInterval_horizontal_match line 464
  40. lemma OAI.Thomason.GrayRecursive.constantInterval_horizontalDiagonalOne line 471
  41. lemma OAI.Thomason.GrayRecursive.constantInterval_horizontalDiagonalTwo line 487
  42. lemma OAI.Thomason.GrayRecursive.horizontalCylinder_endpoint line 503
  43. lemma OAI.Thomason.GrayRecursive.horizontalCylinder_edge line 512
  44. lemma OAI.Thomason.GrayRecursive.horizontalCylinder_up line 520
  45. lemma OAI.Thomason.GrayRecursive.horizontalCylinder_constant line 530
  46. lemma OAI.Thomason.GrayRecursive.faceMap_vertex line 558
  47. lemma OAI.Thomason.GrayRecursive.faceMap_suspend line 566
  48. lemma OAI.Thomason.GrayRecursive.cylinderHom_atEnd line 577
  49. lemma OAI.Thomason.GrayRecursive.tensorFace_edge line 583
  50. lemma OAI.Thomason.GrayRecursive.tensorFace_up line 588
  51. def OAI.Thomason.GrayRecursive.rectangleDiagramOfTop line 640
  52. def OAI.Thomason.GrayRecursive.FaceMatching line 695
  53. def OAI.Thomason.GrayRecursive.globeComposite line 701
  54. lemma OAI.Thomason.GrayRecursive.globeComposite_top line 711
  55. lemma OAI.Thomason.GrayRecursive.globeMatching_vertex line 717
  56. lemma OAI.Thomason.GrayRecursive.globeComposite_vertex line 735
  57. lemma OAI.Thomason.GrayRecursive.globeComposite_natural line 749
  58. lemma OAI.Thomason.GrayRecursive.FaceMatching.ends line 761
  59. lemma OAI.Thomason.GrayRecursive.FaceMatching.edges line 772
  60. lemma OAI.Thomason.GrayRecursive.FaceMatching.vertices line 778
  61. lemma OAI.Thomason.GrayRecursive.FaceMatching.natural line 784