OAI/CategoryTheory/Thomason/GrayGenerators.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Gray Generators.

  1. instance OAI.Thomason.GrayTwo.(instance at line 15) line 15
  2. lemma OAI.Thomason.GrayTwo.code_injective line 19
  3. def OAI.Thomason.GrayTwo.cell line 21
  4. lemma OAI.Thomason.GrayTwo.coordinates_cell line 23
  5. lemma OAI.Thomason.GrayTwo.cell_injective line 26
  6. lemma OAI.Thomason.GrayTwo.cell_surjective line 30
  7. def OAI.Thomason.GrayTwo.cellEquiv line 36
  8. def OAI.Thomason.GrayTwo.faceIndex line 39
  9. lemma OAI.Thomason.GrayTwo.faceIndex_three_add line 49
  10. lemma OAI.Thomason.GrayTwo.truncate_cell line 52
  11. lemma OAI.Thomason.GrayTwo.cell_composable_iff line 70
  12. lemma OAI.Thomason.OmegaCategory.comp_of_right_source_fixed line 85
  13. def OAI.Thomason.GrayTwo.composite line 103
  14. lemma OAI.Thomason.GrayTwo.composite_match line 108
  15. lemma OAI.Thomason.GrayTwo.composite_eq line 114
  16. lemma OAI.Thomason.GrayTwo.composable_cases line 122
  17. structure OAI.Thomason.GrayTwo.Diagram line 136
  18. lemma OAI.Thomason.GrayTwo.Diagram.source_obj line 148
  19. lemma OAI.Thomason.GrayTwo.Diagram.target_obj line 150
  20. def OAI.Thomason.GrayTwo.Diagram.evaluate line 153
  21. lemma OAI.Thomason.GrayTwo.Diagram.evaluate_cell line 155
  22. lemma OAI.Thomason.GrayTwo.Diagram.evaluate_comp line 158
  23. def OAI.Thomason.GrayTwo.Diagram.lift line 177
  24. lemma OAI.Thomason.GrayTwo.Diagram.lift_cell line 194
  25. lemma OAI.Thomason.GrayTwo.functor_ext line 199
  26. def OAI.Thomason.GrayTwo.diagramOfFunctor line 206
  27. lemma OAI.Thomason.GrayTwo.diagramOfFunctor_lift line 216
  28. abbrev OAI.Thomason.OmegaCategory.join line 232
  29. lemma OAI.Thomason.OmegaCategory.join_eq line 235
  30. lemma OAI.Thomason.OmegaCategory.join_source_le line 239
  31. lemma OAI.Thomason.OmegaCategory.join_target_le line 243
  32. lemma OAI.Thomason.OmegaCategory.join_source_gt line 247
  33. lemma OAI.Thomason.OmegaCategory.join_target_gt line 252
  34. lemma OAI.Thomason.OmegaCategory.join_left_unit line 258
  35. lemma OAI.Thomason.OmegaCategory.join_right_unit line 262
  36. lemma OAI.Thomason.OmegaCategory.join_assoc line 267
  37. lemma OAI.Thomason.OmegaCategory.join_four line 275
  38. lemma OAI.Thomason.OmegaCategory.join_four_middle line 283
  39. lemma OAI.Thomason.OmegaCategory.join_interchange line 292
  40. lemma OAI.Thomason.OmegaCategory.join_factor_right line 314
  41. lemma OAI.Thomason.OmegaCategory.join_factor_left line 328
  42. lemma OAI.Thomason.OmegaCategory.join_middle line 342
  43. lemma OAI.Thomason.OmegaCategory.join_whisker_right line 348
  44. lemma OAI.Thomason.OmegaCategory.join_whisker_left line 358
  45. lemma OAI.Thomason.OmegaCategory.Functor.map_join line 368
  46. lemma OAI.Thomason.GrayTwo.Diagram.obj_composite line 387
  47. lemma OAI.Thomason.GrayTwo.Diagram.obj5 line 392
  48. lemma OAI.Thomason.GrayTwo.Diagram.obj7 line 393
  49. lemma OAI.Thomason.GrayTwo.Diagram.obj8 line 394
  50. lemma OAI.Thomason.GrayTwo.Diagram.obj9 line 395
  51. lemma OAI.Thomason.GrayTwo.Diagram.obj11 line 396
  52. lemma OAI.Thomason.GrayTwo.Diagram.obj13 line 397
  53. lemma OAI.Thomason.GrayTwo.Diagram.obj14 line 398
  54. lemma OAI.Thomason.GrayTwo.Diagram.obj15 line 399
  55. lemma OAI.Thomason.GrayTwo.glue_source line 406
  56. lemma OAI.Thomason.GrayTwo.glue_target line 411
  57. def OAI.Thomason.GrayTwo.pastedObj line 416
  58. lemma OAI.Thomason.GrayTwo.pasted_match9 line 454
  59. lemma OAI.Thomason.GrayTwo.pasted_match11 line 462
  60. lemma OAI.Thomason.GrayTwo.pasted_source_zero line 470
  61. lemma OAI.Thomason.GrayTwo.pasted_target_zero line 479
  62. lemma OAI.Thomason.GrayTwo.pasted_source_one line 488
  63. lemma OAI.Thomason.GrayTwo.pasted_target_one line 497
  64. lemma OAI.Thomason.GrayTwo.pasted_source_three line 506
  65. lemma OAI.Thomason.GrayTwo.pasted_source_two_others line 515
  66. lemma OAI.Thomason.GrayTwo.pasted_target_two_others line 525
  67. lemma OAI.Thomason.GrayTwo.pasted_source_coherence line 535
  68. lemma OAI.Thomason.GrayTwo.pasted_source_two_top line 581
  69. lemma OAI.Thomason.GrayTwo.pasted_target_coherence line 588
  70. lemma OAI.Thomason.GrayTwo.pasted_target_two_top line 632
  71. lemma OAI.Thomason.GrayTwo.pasted_faces line 639
  72. def OAI.Thomason.GrayTwo.paste line 658
  73. lemma OAI.Thomason.GrayTwo.paste_obj line 665
  74. def OAI.Thomason.GrayTwo.Diagram.map line 682
  75. lemma OAI.Thomason.GrayTwo.Diagram.map_obj line 691
  76. lemma OAI.Thomason.GrayTwo.map_pastedObj line 696
  77. def OAI.Thomason.GrayTwo.generators line 711
  78. lemma OAI.Thomason.GrayTwo.functor_ext_generators line 713