OAI/CategoryTheory/Thomason/HomotopyExtension.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Homotopy Extension.

  1. def OAI.Thomason.TopologicalCylinder.minimum line 17
  2. lemma OAI.Thomason.TopologicalCylinder.minimum_nonneg line 20
  3. lemma OAI.Thomason.TopologicalCylinder.minimum_le line 23
  4. lemma OAI.Thomason.TopologicalCylinder.minimum_attained line 26
  5. lemma OAI.Thomason.TopologicalCylinder.continuous_minimum line 30
  6. def OAI.Thomason.TopologicalCylinder.denominator line 34
  7. lemma OAI.Thomason.TopologicalCylinder.denominator_pos line 37
  8. lemma OAI.Thomason.TopologicalCylinder.denominator_le_one line 41
  9. lemma OAI.Thomason.TopologicalCylinder.continuous_denominator line 47
  10. def OAI.Thomason.TopologicalCylinder.time line 51
  11. lemma OAI.Thomason.TopologicalCylinder.continuous_time line 62
  12. def OAI.Thomason.TopologicalCylinder.space line 67
  13. def OAI.Thomason.TopologicalCylinder.bottomSides line 92
  14. lemma OAI.Thomason.TopologicalCylinder.retract_mem line 95
  15. def OAI.Thomason.TopologicalCylinder.retract line 114
  16. lemma OAI.Thomason.TopologicalCylinder.retract_fixed line 118
  17. def OAI.Thomason.TopologicalCylinder.boundarySet line 136
  18. lemma OAI.Thomason.TopologicalCylinder.minimum_eq_zero line 138
  19. lemma OAI.Thomason.TopologicalCylinder.isClosed_boundarySet line 142
  20. def OAI.Thomason.TopologicalCylinder.bottomPiece line 153
  21. lemma OAI.Thomason.TopologicalCylinder.isClosed_bottomPiece line 159
  22. lemma OAI.Thomason.TopologicalCylinder.bottomPiece_cover line 164
  23. def OAI.Thomason.TopologicalCylinder.bottomPieceValue line 171
  24. lemma OAI.Thomason.TopologicalCylinder.bottomPieceValue_agree line 181
  25. def OAI.Thomason.TopologicalCylinder.bottomValue line 195
  26. def OAI.Thomason.TopologicalCylinder.extend line 200
  27. lemma OAI.Thomason.TopologicalCylinder.extend_onRoof line 204
  28. lemma OAI.Thomason.TopologicalCylinder.extend_zero line 209
  29. lemma OAI.Thomason.TopologicalCylinder.extend_side line 216
  30. lemma OAI.Thomason.TopologicalCylinder.boundary_faces_agree line 223
  31. def OAI.Thomason.TopologicalCylinder.boundaryValue line 276
  32. lemma OAI.Thomason.TopologicalCylinder.boundaryValue_face line 287
  33. lemma OAI.Thomason.TopologicalCylinder.boundaryValue_square line 298
  34. def OAI.Thomason.TopologicalCylinder.pathStart line 312
  35. theorem OAI.Thomason.TopologicalCylinder.singular_pathStart_boundary_rlp line 315
  36. theorem OAI.Thomason.TopologicalCylinder.realization_mono_homotopy_extension line 367
  37. lemma OAI.Thomason.WeakHomotopy.Equivalence.middle line 387
  38. lemma OAI.Thomason.simplicialWeakEquivalences_middle line 423
  39. lemma OAI.Thomason.CoherentGluing.zeroFactor_one line 444
  40. lemma OAI.Thomason.CoherentGluing.extend_one line 456
  41. def OAI.Thomason.CoherentGluing.toHomotopy line 489
  42. lemma OAI.Thomason.CoherentGluing.pushout_weak line 501
  43. def OAI.Thomason.HornSubdivision.endpoint line 591
  44. lemma OAI.Thomason.HornSubdivision.endpoint_natural line 594
  45. lemma OAI.Thomason.HornSubdivision.endpoint_zero line 598
  46. lemma OAI.Thomason.HornSubdivision.endpoint_one line 608
  47. lemma OAI.Thomason.HornSubdivision.cylinder_lift line 619
  48. lemma OAI.Thomason.HornSubdivision.anodyne_of_coherent_span line 652
  49. def OAI.Thomason.HornSubdivision.orderCylinder line 694
  50. def OAI.Thomason.HornSubdivision.orderCylinderCat line 704
  51. def OAI.Thomason.HornSubdivision.orderHomotopy line 710
  52. lemma OAI.Thomason.HornSubdivision.orderHomotopy_coherent line 732
  53. lemma OAI.Thomason.HornSubdivision.hornFaceInclusion_anodyne line 749