OAI/CategoryTheory/Thomason/SubdivisionMaps.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Subdivision Maps.

  1. lemma OAI.Thomason.TopologicalHorn.minimum_le_one line 16
  2. def OAI.Thomason.TopologicalHorn.prismDenominator line 22
  3. lemma OAI.Thomason.TopologicalHorn.prismDenominator_pos line 25
  4. lemma OAI.Thomason.TopologicalHorn.prismDenominator_le_one line 30
  5. lemma OAI.Thomason.TopologicalHorn.continuous_prismDenominator line 36
  6. def OAI.Thomason.TopologicalHorn.prismTime line 40
  7. def OAI.Thomason.TopologicalHorn.prismSpace line 53
  8. lemma OAI.Thomason.TopologicalHorn.continuous_prismTime line 91
  9. def OAI.Thomason.TopologicalHorn.prismRoof line 96
  10. lemma OAI.Thomason.TopologicalHorn.prism_mem_roof line 99
  11. def OAI.Thomason.TopologicalHorn.prismRetract line 127
  12. lemma OAI.Thomason.TopologicalHorn.prismRetract_fixed line 131
  13. lemma OAI.Thomason.TopologicalHorn.isClosed_horn line 165
  14. def OAI.Thomason.TopologicalHorn.roofPiece line 176
  15. lemma OAI.Thomason.TopologicalHorn.isClosed_roofPiece line 180
  16. lemma OAI.Thomason.TopologicalHorn.roofPiece_cover line 186
  17. def OAI.Thomason.TopologicalHorn.roofPieceValue line 194
  18. lemma OAI.Thomason.TopologicalHorn.roofPieceValue_agree line 202
  19. def OAI.Thomason.TopologicalHorn.roofValue line 235
  20. def OAI.Thomason.TopologicalHorn.prismExtend line 240
  21. lemma OAI.Thomason.TopologicalHorn.prismExtend_onRoof line 244
  22. lemma OAI.Thomason.TopologicalHorn.prismExtend_zero line 249
  23. lemma OAI.Thomason.TopologicalHorn.prismExtend_one line 256
  24. lemma OAI.Thomason.TopologicalHorn.prismExtend_side line 263
  25. lemma OAI.Thomason.TopologicalHorn.singularValue_post line 283
  26. lemma OAI.Thomason.TopologicalHorn.hornValue_square line 287
  27. abbrev OAI.Thomason.TopologicalHorn.PathSpace line 302
  28. abbrev OAI.Thomason.TopologicalHorn.EndpointSpace line 303
  29. def OAI.Thomason.TopologicalHorn.pathEndpoints line 305
  30. theorem OAI.Thomason.TopologicalHorn.singular_path_fibration line 308
  31. lemma OAI.Thomason.TopologicalHorn.anodyne_top_extension line 369
  32. theorem OAI.Thomason.TopologicalHorn.anodyne_weak_equivalence line 383
  33. def OAI.Thomason.SimplicialCylinder.hornOneIso line 432
  34. lemma OAI.Thomason.SimplicialCylinder.delta_one_anodyne line 446
  35. def OAI.Thomason.SimplicialCylinder.zeroFactorIso line 454
  36. lemma OAI.Thomason.SimplicialCylinder.endpoint_anodyne line 463
  37. lemma OAI.Thomason.SimplicialCylinder.endpoint_weak line 491
  38. def OAI.Thomason.SimplicialCylinder.Ends line 509
  39. def OAI.Thomason.SimplicialCylinder.endsMap line 515
  40. def OAI.Thomason.SimplicialCylinder.endsInclusion line 523
  41. instance OAI.Thomason.SimplicialCylinder.endsInclusion_mono line 526
  42. theorem OAI.Thomason.SimplicialCylinder.boundary_rlp_weak line 545
  43. instance OAI.Thomason.KanQuillen.boundary_small line 592
  44. instance OAI.Thomason.KanQuillen.boundary_smallCardinal line 598
  45. instance OAI.Thomason.KanQuillen.boundary_smallObject line 605
  46. lemma OAI.Thomason.KanQuillen.boundary_left_class line 608
  47. lemma OAI.Thomason.KanQuillen.anodyne_monomorphism line 616
  48. lemma OAI.Thomason.KanQuillen.boundary_right_fibrations line 621
  49. lemma OAI.Thomason.KanQuillen.boundary_right_weak line 625
  50. lemma OAI.Thomason.KanQuillen.anodyne_weak line 628
  51. theorem OAI.Thomason.KanQuillen.boundary_weakFactorization line 631
  52. theorem OAI.Thomason.KanQuillen.horn_weakFactorization line 636
  53. def OAI.Thomason.KanQuillen.factorization_cof_weakFib line 641
  54. def OAI.Thomason.KanQuillen.factorization_weakCof_fib line 652
  55. lemma OAI.Thomason.Subdivision.chain_has_greatest line 677
  56. def OAI.Thomason.Subdivision.chainGreatest line 685
  57. lemma OAI.Thomason.Subdivision.chainGreatest_mem line 688
  58. lemma OAI.Thomason.Subdivision.le_chainGreatest line 691
  59. def OAI.Thomason.Subdivision.chainLast line 694
  60. lemma OAI.Thomason.Subdivision.chainGreatest_map line 698
  61. def OAI.Thomason.Subdivision.chainLastNat line 708
  62. def OAI.Thomason.Subdivision.OldChains line 716
  63. def OAI.Thomason.Subdivision.MeetingChains line 718
  64. instance OAI.Thomason.Subdivision.(instance at line 720) line 720
  65. instance OAI.Thomason.Subdivision.(instance at line 721) line 721
  66. def OAI.Thomason.Subdivision.chainInclusion line 723
  67. def OAI.Thomason.Subdivision.chainIntersection line 729
  68. lemma OAI.Thomason.Subdivision.chainIntersection_adjunction line 748
  69. lemma OAI.Thomason.Subdivision.chainIntersection_retraction line 758
  70. lemma OAI.Thomason.Subdivision.oldChains_sieve line 765
  71. lemma OAI.Thomason.Subdivision.meetingChains_cosieve line 769
  72. lemma OAI.Thomason.Subdivision.meetingChains_upward line 774
  73. def OAI.Thomason.Subdivision.simplexNerveIso line 804
  74. def OAI.Thomason.Subdivision.simplexLastVertex line 816
  75. def OAI.Thomason.Subdivision.lastVertex line 820
  76. lemma OAI.Thomason.Subdivision.lastVertex_stdSimplex line 823
  77. def OAI.Thomason.Subdivision.exComparison line 831
  78. lemma OAI.Thomason.Subdivision.exComparison_mate line 840