OAI/CategoryTheory/Thomason/BoundedCylinders.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Bounded Cylinders.

  1. lemma OAI.Thomason.DirectedComplex.CylinderTables.truncate_zero_ext line 16
  2. lemma OAI.Thomason.DirectedComplex.CylinderTables.truncate_one_ext line 23
  3. def OAI.Thomason.DirectedComplex.CylinderTables.tableSandwich line 33
  4. lemma OAI.Thomason.DirectedComplex.CylinderTables.tableSandwich_match_left line 38
  5. lemma OAI.Thomason.DirectedComplex.CylinderTables.tableSandwich_match_right line 44
  6. lemma OAI.Thomason.DirectedComplex.CylinderTables.tableSandwich_zero line 53
  7. lemma OAI.Thomason.DirectedComplex.CylinderTables.tableSandwich_succ line 61
  8. lemma OAI.Thomason.DirectedComplex.CylinderTables.tableSandwich_bounded line 72
  9. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossingProfile_face_zero line 89
  10. lemma OAI.Thomason.DirectedComplex.CylinderTables.profile_left_zero line 93
  11. lemma OAI.Thomason.DirectedComplex.CylinderTables.profile_right_zero line 100
  12. lemma OAI.Thomason.DirectedComplex.CylinderTables.face_one_label line 107
  13. def OAI.Thomason.DirectedComplex.CylinderTables.profileEdge line 110
  14. lemma OAI.Thomason.DirectedComplex.CylinderTables.profileEdge_bounded line 114
  15. lemma OAI.Thomason.DirectedComplex.CylinderTables.profileEdge_zero line 121
  16. lemma OAI.Thomason.DirectedComplex.CylinderTables.profileEdge_one line 134
  17. def OAI.Thomason.DirectedComplex.CylinderTables.twoRight line 143
  18. def OAI.Thomason.DirectedComplex.CylinderTables.twoMiddle line 146
  19. def OAI.Thomason.DirectedComplex.CylinderTables.twoLeft line 149
  20. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoRight_matches line 154
  21. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoMiddle_matches line 160
  22. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoLeft_matches line 166
  23. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoRight_zero line 172
  24. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoMiddle_zero line 180
  25. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoLeft_zero line 188
  26. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoRight_one line 196
  27. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoMiddle_one line 205
  28. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoLeft_one line 212
  29. lemma OAI.Thomason.DirectedComplex.CylinderTables.profileCross_two_zero line 224
  30. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoRight_two line 227
  31. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoMiddle_two line 237
  32. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoLeft_two line 246
  33. lemma OAI.Thomason.DirectedComplex.CylinderTables.profileEdge_bounded_two line 255
  34. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoRight_bounded line 261
  35. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoMiddle_bounded line 267
  36. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoLeft_bounded line 272
  37. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoRight_source line 279
  38. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoRightMiddle_match line 288
  39. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoMiddleLeft_match line 297
  40. lemma OAI.Thomason.DirectedComplex.CylinderTables.twoRightMiddleLeft_match line 306
  41. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_two_factor line 312
  42. def OAI.Thomason.GrayRecursive.IntervalHom.TwoLiftable line 339
  43. lemma OAI.Thomason.GrayRecursive.IntervalHom.TwoLiftable.endpoint line 343
  44. lemma OAI.Thomason.GrayRecursive.IntervalHom.TwoLiftable.vertical line 349
  45. lemma OAI.Thomason.GrayRecursive.IntervalHom.TwoLiftable.comp line 358
  46. lemma OAI.Thomason.GrayRecursive.IntervalHom.TwoLiftable.join line 376
  47. lemma OAI.Thomason.GrayRecursive.IntervalHom.TwoLiftable.sandwich line 382
  48. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_crossing_twocells_surjective line 390
  49. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_twocells_surjective line 409
  50. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_poset_twocells_surjective line 423
  51. def OAI.Thomason.GrayRecursive.IntervalHom.verticalCell line 439
  52. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_bounded line 442
  53. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_natural line 449
  54. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_verticalCell line 453
  55. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_zero line 459
  56. lemma OAI.Thomason.GrayRecursive.IntervalHom.vertical_one_face line 461
  57. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorUnitCell_face line 475
  58. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_vertical_face line 481
  59. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_dimension_independent line 502
  60. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_vertical_vertex line 511
  61. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_one_face line 523
  62. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_matching line 551
  63. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_comp line 559
  64. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_one_comp line 575
  65. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_cells_induction line 608
  66. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_functor_ext line 634
  67. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_eq_of_value line 650
  68. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_bounded_of_bounded line 660
  69. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_truncated line 666
  70. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_bounded_cells_induction line 708