OAI/CategoryTheory/Thomason/RectangleComposition.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Rectangle Composition.

  1. structure OAI.Thomason.GrayRecursive.RectangleDiagram line 15
  2. def OAI.Thomason.GrayRecursive.RectangleDiagram.interpret line 31
  3. def OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap line 36
  4. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_eval line 39
  5. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_endpoint line 43
  6. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_edge line 45
  7. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_up line 47
  8. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_truncate line 50
  9. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_composable line 82
  10. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_fixed line 88
  11. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_comp_of_left_fixed line 92
  12. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_comp_of_right_fixed line 99
  13. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_comp_positive line 106
  14. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_comp_zero line 153
  15. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.cellMap_comp line 194
  16. def OAI.Thomason.GrayRecursive.RectangleDiagram.lift line 201
  17. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.lift_endpoint line 207
  18. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.lift_edge line 209
  19. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.lift_up line 211
  20. def OAI.Thomason.GrayRecursive.extractDiagonal line 226
  21. def OAI.Thomason.GrayRecursive.rectangleDiagramOfFunctor line 246
  22. lemma OAI.Thomason.GrayRecursive.functor_ext_rectangle line 271
  23. lemma OAI.Thomason.GrayRecursive.rectangleDiagramOfFunctor_lift line 284
  24. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.lift_unique line 291
  25. def OAI.Thomason.OmegaCategory.homCompose line 312
  26. lemma OAI.Thomason.OmegaCategory.homCompose_map line 347
  27. def OAI.Thomason.OmegaCategory.constantAt line 351
  28. def OAI.Thomason.OmegaCategory.constantHom line 360
  29. def OAI.Thomason.OmegaCategory.homCast line 364
  30. lemma OAI.Thomason.GrayRecursive.globe_zero_unique line 384
  31. lemma OAI.Thomason.GrayRecursive.globe_one_cases line 391
  32. def OAI.Thomason.GrayRecursive.zeroCylinderMap line 398
  33. lemma OAI.Thomason.GrayRecursive.zeroCylinderMap_top line 402
  34. lemma OAI.Thomason.GrayRecursive.zeroCylinderMap_vertex line 406
  35. lemma OAI.Thomason.GrayRecursive.zeroCylinderMap_bijective line 421
  36. def OAI.Thomason.GrayRecursive.zeroCylinderIso line 450
  37. def OAI.Thomason.GrayRecursive.zeroCylinderLift line 453
  38. lemma OAI.Thomason.GrayRecursive.zeroCylinderLift_vertical line 457
  39. lemma OAI.Thomason.GrayRecursive.zeroCylinderLift_endpoint line 467
  40. def OAI.Thomason.GrayRecursive.IntervalMatching line 491
  41. structure OAI.Thomason.GrayRecursive.IntervalComposition line 495
  42. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.seam_edge line 509
  43. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.edge_end_matching line 512
  44. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.end_edge_matching line 517
  45. def OAI.Thomason.GrayRecursive.RectangleDiagram.concatDiagonalOne line 522
  46. def OAI.Thomason.GrayRecursive.RectangleDiagram.concatDiagonalTwo line 527
  47. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.concatDiagonal_matching line 532
  48. def OAI.Thomason.GrayRecursive.RectangleDiagram.concat line 542
  49. def OAI.Thomason.GrayRecursive.IntervalComposition.zero line 575
  50. def OAI.Thomason.GrayRecursive.IntervalComposition.succ line 612
  51. def OAI.Thomason.GrayRecursive.intervalComposition line 620
  52. def OAI.Thomason.GrayRecursive.RectangleDiagram.map line 638
  53. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.map_ofFunctor line 656
  54. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.lift_map line 660
  55. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.map_concatDiagonalOne line 670
  56. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.map_concatDiagonalTwo line 681
  57. abbrev OAI.Thomason.GrayRecursive.concatInterval line 694
  58. lemma OAI.Thomason.GrayRecursive.concatInterval_endpoint line 698
  59. lemma OAI.Thomason.GrayRecursive.concatInterval_zero_vertical line 703
  60. lemma OAI.Thomason.GrayRecursive.concatInterval_succ_edge line 709
  61. lemma OAI.Thomason.GrayRecursive.concatInterval_succ_up line 715
  62. lemma OAI.Thomason.GrayRecursive.zero_interval_seam line 723
  63. lemma OAI.Thomason.GrayRecursive.concatInterval_natural line 735