OAI/CategoryTheory/Thomason/GlobularGeneration.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Globular Generation.

  1. def OAI.Thomason.GrayRecursive.corner line 15
  2. lemma OAI.Thomason.GrayRecursive.diagonal_iff_boundaries line 35
  3. lemma OAI.Thomason.GrayRecursive.truncate_diagonal line 46
  4. lemma OAI.Thomason.GrayRecursive.comp_diagonal line 51
  5. lemma OAI.Thomason.GrayRecursive.down_truncate line 57
  6. lemma OAI.Thomason.GrayRecursive.down_comp line 63
  7. abbrev OAI.Thomason.GrayRecursive.diagonalHom line 72
  8. def OAI.Thomason.GrayRecursive.downFunctor line 75
  9. lemma OAI.Thomason.GrayRecursive.downFunctor_bijective line 81
  10. def OAI.Thomason.GrayRecursive.diagonalIso line 90
  11. lemma OAI.Thomason.GrayRecursive.diagonalIso_inverse line 93
  12. lemma OAI.Thomason.GlobeComplex.positive_cycle_zero line 112
  13. lemma OAI.Thomason.GlobeComplex.positive_add_zero line 120
  14. def OAI.Thomason.GrayRecursive.sideRow line 140
  15. def OAI.Thomason.GrayRecursive.crossRow line 144
  16. def OAI.Thomason.GrayRecursive.project line 147
  17. lemma OAI.Thomason.GrayRecursive.project_row line 150
  18. lemma OAI.Thomason.GrayRecursive.side_positive line 153
  19. lemma OAI.Thomason.GrayRecursive.cross_positive line 159
  20. lemma OAI.Thomason.GrayRecursive.cross_boundary line 162
  21. lemma OAI.Thomason.GrayRecursive.left_boundary line 166
  22. lemma OAI.Thomason.GrayRecursive.right_boundary line 173
  23. lemma OAI.Thomason.GrayRecursive.side_augmentation line 180
  24. lemma OAI.Thomason.GrayRecursive.side_mass_vertex line 183
  25. lemma OAI.Thomason.GrayRecursive.cross_mass_vertex line 190
  26. lemma OAI.Thomason.GrayRecursive.interval_monotone line 198
  27. lemma OAI.Thomason.GrayRecursive.cross_succ_eq_zero_of_constant line 204
  28. lemma OAI.Thomason.GrayRecursive.no_cross_of_stationary_interval line 213
  29. lemma OAI.Thomason.GrayRecursive.no_side_of_empty_vertex line 223
  30. lemma OAI.Thomason.GrayRecursive.endpoint_of_stationary_interval line 235
  31. lemma OAI.Thomason.GrayRecursive.crossing_sides line 268
  32. lemma OAI.Thomason.GrayRecursive.crossing_vertices line 281
  33. lemma OAI.Thomason.GrayRecursive.crossing_diagonal line 291
  34. lemma OAI.Thomason.GrayRecursive.crossing_vertical line 306
  35. lemma OAI.Thomason.GrayRecursive.table_cases line 349
  36. def OAI.Thomason.GlobeComplex.suspendTable line 373
  37. lemma OAI.Thomason.GlobeComplex.suspendTable_zero line 401
  38. lemma OAI.Thomason.GlobeComplex.suspendTable_succ line 404
  39. lemma OAI.Thomason.GlobeComplex.suspendTable_truncate line 407
  40. lemma OAI.Thomason.GlobeComplex.suspendTable_top line 417
  41. lemma OAI.Thomason.GlobeComplex.suspendTable_eq_face line 433
  42. def OAI.Thomason.GrayRecursive.atEnd line 448
  43. def OAI.Thomason.GrayRecursive.vertex line 451
  44. lemma OAI.Thomason.GrayRecursive.vertex_zero line 453
  45. lemma OAI.Thomason.GrayRecursive.vertex_succ line 457
  46. lemma OAI.Thomason.GrayRecursive.vertexWeights_one_zero line 460
  47. lemma OAI.Thomason.GrayRecursive.vertexWeights_zero_one line 466
  48. lemma OAI.Thomason.GrayRecursive.up_truncate line 472
  49. lemma OAI.Thomason.GrayRecursive.up_composable line 481
  50. lemma OAI.Thomason.GrayRecursive.up_comp line 486
  51. lemma OAI.Thomason.GrayRecursive.up_endpoint_left_matching line 497
  52. lemma OAI.Thomason.GrayRecursive.up_endpoint_right_matching line 507
  53. lemma OAI.Thomason.GrayRecursive.up_endpoint_false line 517
  54. lemma OAI.Thomason.GrayRecursive.up_endpoint_true line 547
  55. lemma OAI.Thomason.GrayRecursive.up_vertical line 574
  56. lemma OAI.Thomason.GrayRecursive.table_zero_cases line 597
  57. lemma OAI.Thomason.GrayRecursive.generated line 610
  58. lemma OAI.Thomason.DirectedComplex.Table.fixed_of_rows_zero line 651
  59. lemma OAI.Thomason.DirectedComplex.Table.fixed_iff_rows_zero line 665
  60. lemma OAI.Thomason.GrayRecursive.up_injective line 680
  61. lemma OAI.Thomason.GrayRecursive.up_fixed_iff line 686
  62. lemma OAI.Thomason.GrayRecursive.project_fixed line 691
  63. lemma OAI.Thomason.GrayRecursive.atEnd_fixed line 697
  64. lemma OAI.Thomason.GrayRecursive.suspend_fixed line 703
  65. lemma OAI.Thomason.GrayRecursive.vertex_fixed line 707
  66. lemma OAI.Thomason.GrayRecursive.vertical_fixed line 710
  67. lemma OAI.Thomason.GrayRecursive.vertical_fixed_iff line 720
  68. lemma OAI.Thomason.GrayRecursive.zero_is_endpoint line 731
  69. lemma OAI.Thomason.GrayRecursive.generated_bounded line 740
  70. lemma OAI.Thomason.GrayRecursive.functor_ext line 790
  71. lemma OAI.Thomason.GrayRecursive.functor_ext_truncated line 802