OAI/CategoryTheory/Thomason/StationaryCylinders.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Stationary Cylinders.

  1. def OAI.Thomason.GrayRecursive.endGlobe line 15
  2. lemma OAI.Thomason.GrayRecursive.endGlobe_map line 20
  3. lemma OAI.Thomason.GrayRecursive.stationary_left_matching line 24
  4. lemma OAI.Thomason.GrayRecursive.stationary_right_matching line 30
  5. def OAI.Thomason.GrayRecursive.IntervalUnits line 36
  6. lemma OAI.Thomason.GrayRecursive.zero_vertical_source line 41
  7. lemma OAI.Thomason.GrayRecursive.zero_vertical_target line 48
  8. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.vertex_fixed line 58
  9. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.vertex_target_fixed line 63
  10. lemma OAI.Thomason.GrayRecursive.concatInterval_units line 68
  11. lemma OAI.Thomason.GrayRecursive.concatInterval_left_unit line 164
  12. lemma OAI.Thomason.GrayRecursive.concatInterval_right_unit line 168
  13. lemma OAI.Thomason.GrayRecursive.concatInterval_homCompose_stationary_left line 183
  14. lemma OAI.Thomason.GrayRecursive.concatInterval_homCompose_stationary_right line 193
  15. def OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.beforeGlobe line 209
  16. def OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.suffix line 213
  17. def OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.A line 217
  18. def OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.B line 218
  19. def OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.C line 219
  20. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.B_map line 221
  21. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.AB line 238
  22. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.BC line 247
  23. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.left_one_map line 257
  24. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.left_two_map line 265
  25. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.right_one_map line 279
  26. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.HorizontalAssociativity.right_two_map line 294
  27. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.horizontal_associative line 310
  28. lemma OAI.Thomason.GrayRecursive.horizontalCylinder_associative line 345
  29. lemma OAI.Thomason.GrayRecursive.pasteCylinder_val_congr line 368
  30. lemma OAI.Thomason.GrayRecursive.pasteCylinder_associative line 385
  31. def OAI.Thomason.GrayRecursive.restrictCylinder line 478
  32. lemma OAI.Thomason.GrayRecursive.restrictCylinder_endpoint line 482
  33. lemma OAI.Thomason.GrayRecursive.restrictCylinder_edge line 487
  34. lemma OAI.Thomason.GrayRecursive.restrictCylinder_up line 492
  35. lemma OAI.Thomason.GrayRecursive.restrictCylinder_self line 497
  36. lemma OAI.Thomason.GrayRecursive.IntervalMatching.restrict line 507
  37. lemma OAI.Thomason.GrayRecursive.concatInterval_face line 514
  38. lemma OAI.Thomason.GrayRecursive.functor_ext_zero_cylinder line 586
  39. lemma OAI.Thomason.GrayRecursive.restrictCylinder_endpoint_top line 598
  40. lemma OAI.Thomason.GrayRecursive.restrictCylinder_zero_vertical line 607
  41. lemma OAI.Thomason.GrayRecursive.pasteCylinder_zero_edge line 615
  42. lemma OAI.Thomason.GrayRecursive.pasteCylinder_zero_up line 621
  43. lemma OAI.Thomason.GrayRecursive.pasteCylinder_lower_face line 630