OAI/CategoryTheory/Thomason/KanTowers.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Kan Towers.

  1. lemma OAI.Thomason.AttachmentComparison.nerve_mono_orderMap line 15
  2. lemma OAI.Thomason.AttachmentComparison.one_nerve_mono_orderMap line 23
  3. def OAI.Thomason.AttachmentComparison.upward line 48
  4. abbrev OAI.Thomason.AttachmentComparison.inclusion line 51
  5. abbrev OAI.Thomason.AttachmentComparison.nerveInclusion line 56
  6. def OAI.Thomason.AttachmentComparison.comparison line 59
  7. def OAI.Thomason.AttachmentComparison.targetMap line 68
  8. def OAI.Thomason.AttachmentComparison.sourceMap line 78
  9. def OAI.Thomason.AttachmentComparison.OneStatement line 90
  10. lemma OAI.Thomason.AttachmentComparison.comparison_local_one line 115
  11. abbrev OAI.Thomason.KanPath.Paths line 204
  12. def OAI.Thomason.KanPath.curryR line 206
  13. def OAI.Thomason.KanPath.uncurryR line 208
  14. lemma OAI.Thomason.KanPath.uncurryR_curryR line 211
  15. lemma OAI.Thomason.KanPath.curryR_uncurryR line 218
  16. lemma OAI.Thomason.KanPath.uncurryR_injective line 225
  17. lemma OAI.Thomason.KanPath.uncurryR_pre line 229
  18. lemma OAI.Thomason.KanPath.uncurryR_post line 235
  19. def OAI.Thomason.KanPath.ev line 240
  20. def OAI.Thomason.KanPath.eval₀ line 241
  21. def OAI.Thomason.KanPath.eval₁ line 242
  22. def OAI.Thomason.KanPath.const line 243
  23. lemma OAI.Thomason.KanPath.uncurryR_eq line 245
  24. lemma OAI.Thomason.KanPath.comp_eval₀ line 249
  25. lemma OAI.Thomason.KanPath.comp_eval₁ line 252
  26. lemma OAI.Thomason.KanPath.const_eval₀ line 256
  27. lemma OAI.Thomason.KanPath.const_eval₁ line 259
  28. lemma OAI.Thomason.KanPath.eval₀_naturality line 263
  29. lemma OAI.Thomason.KanPath.eval₁_naturality line 269
  30. def OAI.Thomason.KanPath.minSquare line 276
  31. lemma OAI.Thomason.KanPath.minSquare_left line 287
  32. lemma OAI.Thomason.KanPath.minSquare_right line 298
  33. lemma OAI.Thomason.KanPath.minSquare_bottom line 309
  34. def OAI.Thomason.KanPath.contraction line 321
  35. lemma OAI.Thomason.KanPath.contraction_eval₀ line 333
  36. lemma OAI.Thomason.KanPath.cylinder_lift_ends line 340
  37. abbrev OAI.Thomason.KanPath.MappingPath line 382
  38. def OAI.Thomason.KanPath.left line 383
  39. def OAI.Thomason.KanPath.right line 385
  40. lemma OAI.Thomason.KanPath.fac line 388
  41. lemma OAI.Thomason.KanPath.left_heq line 391
  42. def OAI.Thomason.KanPath.map line 417
  43. lemma OAI.Thomason.KanPath.map_fst line 424
  44. lemma OAI.Thomason.KanPath.map_snd line 429
  45. lemma OAI.Thomason.KanPath.map_right line 435
  46. lemma OAI.Thomason.KanPath.map_comp line 441
  47. lemma OAI.Thomason.KanPath.right_lifting line 451
  48. lemma OAI.Thomason.KanPath.right_fibration line 478
  49. lemma OAI.Thomason.KanPath.relative_lifting line 487
  50. abbrev OAI.Thomason.KanPath.Matching line 532
  51. def OAI.Thomason.KanPath.relative line 535
  52. lemma OAI.Thomason.KanPath.relative_fibration line 540
  53. instance OAI.Thomason.KanPath.mappingPath_kan line 561
  54. lemma OAI.Thomason.KanPath.right_heq line 568
  55. lemma OAI.Thomason.KanPath.right_rlp line 572
  56. lemma OAI.Thomason.KanPath.relative_rlp line 577
  57. abbrev OAI.Thomason.KanTower.edge line 612
  58. def OAI.Thomason.KanTower.cone line 614
  59. lemma OAI.Thomason.KanTower.cone_π line 627
  60. abbrev OAI.Thomason.KanTower.limMap line 634
  61. def OAI.Thomason.KanTower.stage line 636
  62. def OAI.Thomason.KanTower.transition line 639
  63. lemma OAI.Thomason.KanTower.stage_fst line 642
  64. lemma OAI.Thomason.KanTower.stage_snd line 645
  65. lemma OAI.Thomason.KanTower.stage_right line 648
  66. lemma OAI.Thomason.KanTower.transition_fst line 652
  67. lemma OAI.Thomason.KanTower.transition_snd line 655
  68. lemma OAI.Thomason.KanTower.stage_transition line 659
  69. lemma OAI.Thomason.KanTower.path_limit_rlp line 673
  70. lemma OAI.Thomason.KanTower.homotopyEquivalence_limit line 766