OAI/CategoryTheory/Thomason/SubdividedUnit.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Subdivided Unit.

  1. def OAI.Thomason.HornSubdivision.sdSimplexSubcomplexIso line 15
  2. def OAI.Thomason.HornSubdivision.sdSimplexIso line 20
  3. lemma OAI.Thomason.HornSubdivision.sdSimplexSubcomplexIso_naturality line 25
  4. theorem OAI.Thomason.HornSubdivision.sd_horn_anodyne line 36
  5. theorem OAI.Thomason.HornSubdivision.ex_preserves_fibrations line 51
  6. theorem OAI.Thomason.HornSubdivision.sd_preserves_anodyne line 59
  7. lemma OAI.Thomason.HornSubdivision.sdTwice_horn_anodyne line 65
  8. def OAI.Thomason.Subdivision.LastVertexStatement line 79
  9. def OAI.Thomason.LastVertexProof.Homotopic line 92
  10. lemma OAI.Thomason.LastVertexProof.homotopic_of_homotopy line 95
  11. lemma OAI.Thomason.LastVertexProof.homotopic_refl line 98
  12. lemma OAI.Thomason.LastVertexProof.homotopic_symm line 99
  13. lemma OAI.Thomason.LastVertexProof.homotopic_trans line 101
  14. def OAI.Thomason.LastVertexProof.homotopy_pre line 104
  15. def OAI.Thomason.LastVertexProof.homotopy_post line 110
  16. lemma OAI.Thomason.LastVertexProof.homotopic_pre line 114
  17. lemma OAI.Thomason.LastVertexProof.homotopic_post line 122
  18. lemma OAI.Thomason.LastVertexProof.homotopic_weak_iff line 130
  19. def OAI.Thomason.LastVertexProof.intervalEnds line 138
  20. instance OAI.Thomason.LastVertexProof.intervalEnds_mono line 142
  21. def OAI.Thomason.LastVertexProof.endsTensorMap line 171
  22. lemma OAI.Thomason.LastVertexProof.homotopy_of_anodyne_eq line 183
  23. lemma OAI.Thomason.LastVertexProof.extend_anodyne line 211
  24. lemma OAI.Thomason.LastVertexProof.ex_kan line 219
  25. def OAI.Thomason.LastVertexProof.sdCylinderMap line 234
  26. lemma OAI.Thomason.LastVertexProof.sdCylinderMap_zero line 238
  27. lemma OAI.Thomason.LastVertexProof.sdCylinderMap_one line 248
  28. def OAI.Thomason.LastVertexProof.mateHomotopy line 258
  29. lemma OAI.Thomason.LastVertexProof.mate_homotopic line 269
  30. lemma OAI.Thomason.LastVertexProof.unmate_homotopy line 279
  31. lemma OAI.Thomason.LastVertexProof.unmate_homotopic line 306
  32. lemma OAI.Thomason.LastVertexProof.ex_retract line 316
  33. lemma OAI.Thomason.LastVertexProof.mate_lastVertex line 327
  34. lemma OAI.Thomason.LastVertexProof.precomp_lastVertex_surjective line 335
  35. lemma OAI.Thomason.LastVertexProof.precomp_lastVertex_injective line 348
  36. lemma OAI.Thomason.LastVertexProof.lastVertex_weak line 357
  37. theorem OAI.Thomason.Subdivision.lastVertex_weak line 390
  38. lemma OAI.Thomason.Subdivision.sd_map_weak_iff line 392
  39. def OAI.Thomason.SubdividedUnit.OneStatement line 416
  40. def OAI.Thomason.KanHomotopy.sides line 431
  41. lemma OAI.Thomason.KanHomotopy.endpoint_sides line 443
  42. lemma OAI.Thomason.KanHomotopy.ends_sides_post line 449
  43. lemma OAI.Thomason.KanHomotopy.ends_pre line 455
  44. lemma OAI.Thomason.KanHomotopy.square_top_zero line 461
  45. lemma OAI.Thomason.KanHomotopy.square_top_one line 468
  46. lemma OAI.Thomason.KanHomotopy.fill_rectangle line 475
  47. def OAI.Thomason.KanHomotopy.refl line 492
  48. lemma OAI.Thomason.KanHomotopy.homotopy_symm line 495
  49. lemma OAI.Thomason.KanHomotopy.homotopy_trans line 499
  50. lemma OAI.Thomason.KanHomotopy.homotopy_of_homotopic line 503
  51. def OAI.Thomason.KanHomotopy.maxSquare line 511
  52. lemma OAI.Thomason.KanHomotopy.maxSquare_bottom line 522
  53. lemma OAI.Thomason.KanHomotopy.maxSquare_top line 534
  54. lemma OAI.Thomason.KanHomotopy.maxSquare_sides line 547
  55. lemma OAI.Thomason.KanHomotopy.verticalize line 571
  56. lemma OAI.Thomason.KanHomotopy.rlp_of_vertical_retract line 607
  57. def OAI.Thomason.KanHomotopy.IsHomotopyEquivalence line 628
  58. lemma OAI.Thomason.KanHomotopy.homotopy_equivalence_weak line 631
  59. lemma OAI.Thomason.KanHomotopy.rlp_of_homotopy_equivalence line 639