OAI/CategoryTheory/Globular/CylinderObjects.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularFrame.map line 13
  2. def OAI.Grothendieck.GlobularTheory.Model.diskFrame line 27
  3. theorem OAI.Grothendieck.GlobularTheory.Model.diskFrame_source line 36
  4. theorem OAI.Grothendieck.GlobularTheory.Model.diskFrame_target line 41
  5. def OAI.Grothendieck.GlobularTheory.Model.cutoffDiskFrame line 46
  6. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffDiskFrame_source line 51
  7. structure OAI.Grothendieck.CylinderNode line 59
  8. def OAI.Grothendieck.CylinderNode.critical line 70
  9. abbrev OAI.Grothendieck.CylinderNode.nextBoundary line 85
  10. def OAI.Grothendieck.CylinderNode.nextBdEnd line 87
  11. theorem OAI.Grothendieck.CylinderNode.nextBdEnd_left line 93
  12. theorem OAI.Grothendieck.CylinderNode.nextBdEnd_right line 97
  13. abbrev OAI.Grothendieck.TwoEndpoints.first line 107
  14. abbrev OAI.Grothendieck.TwoEndpoints.obj line 108
  15. def OAI.Grothendieck.TwoEndpoints.base line 109
  16. def OAI.Grothendieck.TwoEndpoints.endpoint line 110
  17. theorem OAI.Grothendieck.TwoEndpoints.condition line 113
  18. def OAI.Grothendieck.TwoEndpoints.desc line 121
  19. theorem OAI.Grothendieck.TwoEndpoints.base_desc line 126
  20. theorem OAI.Grothendieck.TwoEndpoints.endpoint_desc line 130
  21. theorem OAI.Grothendieck.TwoEndpoints.hom_ext line 135
  22. theorem OAI.Grothendieck.TwoEndpoints.oneSide_lifting line 143
  23. def OAI.Grothendieck.CylinderNode.stationary line 198
  24. structure OAI.Grothendieck.CylinderNode.Step line 206
  25. def OAI.Grothendieck.CylinderNode.stationaryStep line 213
  26. def OAI.Grothendieck.CylinderNode.criticalStep line 221
  27. def OAI.Grothendieck.GlobularTheory.Model.cylinderFactor line 234
  28. def OAI.Grothendieck.GlobularTheory.Model.completedCylinder line 243
  29. def OAI.Grothendieck.GlobularTheory.Model.cylinderNext line 255
  30. def OAI.Grothendieck.GlobularTheory.Model.cylinderNextStep line 260
  31. def OAI.Grothendieck.GlobularTheory.Model.cylinderNode line 270
  32. theorem OAI.Grothendieck.GlobularTheory.Model.cylinderNode_low line 277
  33. theorem OAI.Grothendieck.GlobularTheory.Model.cylinderNode_critical line 281
  34. theorem OAI.Grothendieck.GlobularTheory.Model.cylinderNode_high line 285
  35. def OAI.Grothendieck.GlobularTheory.Model.cylinderStep line 290
  36. def OAI.Grothendieck.GlobularTheory.Model.cylinderFrame line 305
  37. def OAI.Grothendieck.GlobularTheory.Model.cylinderEndpoint line 319