OAI/CategoryTheory/Thomason/IntervalExtension.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Interval Extension.

  1. lemma OAI.Thomason.GlobeComplex.bounded_table_classification line 16
  2. def OAI.Thomason.GlobeComplex.sourceCollapse line 27
  3. lemma OAI.Thomason.GlobeComplex.sourceCollapse_top line 30
  4. lemma OAI.Thomason.GlobeComplex.sourceCollapse_bounded line 38
  5. lemma OAI.Thomason.GlobeComplex.sourceCollapse_comp_truncated line 46
  6. def OAI.Thomason.GlobeComplex.faceRetraction line 55
  7. lemma OAI.Thomason.GlobeComplex.faceRetraction_top line 58
  8. lemma OAI.Thomason.GlobeComplex.faceMap_retraction line 63
  9. lemma OAI.Thomason.GlobeComplex.retraction_faceMap line 73
  10. lemma OAI.Thomason.GrayRecursive.cylinder_map_endpoint line 90
  11. lemma OAI.Thomason.GrayRecursive.sourceCollapse_cylinder_truncated line 95
  12. def OAI.Thomason.GrayRecursive.truncatedRestrictionEquiv line 110
  13. lemma OAI.Thomason.RightIntervalExtension.internalHom_truncated line 143
  14. def OAI.Thomason.RightIntervalExtension.truncatedCylinderEquiv line 179
  15. lemma OAI.Thomason.RightIntervalExtension.truncatedCylinderEquiv_apply line 187
  16. lemma OAI.Thomason.RightIntervalExtension.truncatedCylinderEquiv_endpoint line 198
  17. def OAI.Thomason.RightIntervalExtension.finiteInternalHom line 221
  18. def OAI.Thomason.RightIntervalExtension.finiteTranspose line 227
  19. def OAI.Thomason.RightIntervalExtension.finiteGlue line 236
  20. lemma OAI.Thomason.RightIntervalExtension.finiteGlue_left line 247
  21. lemma OAI.Thomason.RightIntervalExtension.finiteGlue_right line 257
  22. lemma OAI.Thomason.RightIntervalExtension.finiteCylinder_hom_ext line 268
  23. lemma OAI.Thomason.RightIntervalExtension.finiteGlue_endpoint_left line 282
  24. lemma OAI.Thomason.RightIntervalExtension.finiteGlue_endpoint_right line 294
  25. theorem OAI.Thomason.RightIntervalExtension.finite_stationary_gluing line 308
  26. lemma OAI.Thomason.RightIntervalExtension.finite_stationary_gluing_natural line 351
  27. lemma OAI.Thomason.RightIntervalExtension.simplex_inverse_natural line 400
  28. def OAI.Thomason.RightIntervalExtension.cut line 406
  29. lemma OAI.Thomason.RightIntervalExtension.cut_natural line 410
  30. lemma OAI.Thomason.RightIntervalExtension.cut_endpoint line 419
  31. lemma OAI.Thomason.RightIntervalExtension.cut_projection line 425
  32. def OAI.Thomason.RightIntervalExtension.raiseSimplex line 432
  33. lemma OAI.Thomason.RightIntervalExtension.up_raiseSimplex line 436
  34. lemma OAI.Thomason.RightIntervalExtension.raiseSimplex_precomp line 445
  35. lemma OAI.Thomason.RightIntervalExtension.up_simplexMap line 458
  36. def OAI.Thomason.RightIntervalExtension.nerveCylinderSimplex line 471
  37. lemma OAI.Thomason.RightIntervalExtension.nerveCylinderSimplex_natural line 477
  38. lemma OAI.Thomason.RightIntervalExtension.nerveCylinderSimplex_endpoint line 498
  39. def OAI.Thomason.RightIntervalExtension.nerveCylinder line 512
  40. lemma OAI.Thomason.RightIntervalExtension.nerveCylinder_endpoint line 522
  41. def OAI.Thomason.RightIntervalExtension.nerveHomotopy line 533
  42. lemma OAI.Thomason.RightIntervalExtension.nerveCylinder_postcomp line 546
  43. lemma OAI.Thomason.RightIntervalExtension.nerveCylinder_precomp line 550
  44. lemma OAI.Thomason.RightIntervalExtension.nerveCylinder_projection line 564
  45. lemma OAI.Thomason.RightIntervalExtension.nerveCylinder_stationary line 577
  46. lemma OAI.Thomason.RightIntervalExtension.nerve_weak_iff line 583
  47. def OAI.Thomason.RelativePrismData.finiteImage line 602
  48. def OAI.Thomason.RelativePrismData.finiteImageLeft line 625
  49. def OAI.Thomason.RelativePrismData.finiteImageRight line 629
  50. lemma OAI.Thomason.RelativePrismData.finiteImage_mono line 633
  51. def OAI.Thomason.RelativePrismData.finiteAntihomotopy line 639
  52. def OAI.Thomason.RelativePrismData.finiteCylinderChainMap line 676
  53. lemma OAI.Thomason.RelativePrismData.finiteCylinderChainMap_inclusion line 680
  54. lemma OAI.Thomason.RelativePrismData.finiteCylinderChainMap_natural line 703
  55. lemma OAI.Thomason.RelativePrismData.finiteCylinderChainMap_stationary line 726