OAI/CategoryTheory/Thomason/PosetComparison.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Poset Comparison.

  1. lemma OAI.Thomason.NormalizedChains.grade_induction line 18
  2. def OAI.Thomason.NormalizedChains.homWord line 43
  3. def OAI.Thomason.NormalizedChains.homTotal line 47
  4. lemma OAI.Thomason.NormalizedChains.homTotal_bracket line 50
  5. lemma OAI.Thomason.NormalizedChains.homTotal_grade line 66
  6. lemma OAI.Thomason.NormalizedChains.homTotal_map line 75
  7. lemma OAI.Thomason.NormalizedChains.homTotal_positive line 96
  8. lemma OAI.Thomason.NormalizedChains.homTotal_boundary line 104
  9. lemma OAI.Thomason.NormalizedChains.homTotal_vertex_exists line 143
  10. def OAI.Thomason.NormalizedChains.homVertex line 153
  11. lemma OAI.Thomason.NormalizedChains.homTotal_vertex line 156
  12. lemma OAI.Thomason.NormalizedChains.homVertex_monotone line 160
  13. def OAI.Thomason.NormalizedChains.homVertexOrderHom line 168
  14. lemma OAI.Thomason.NormalizedChains.faces_mem_submodule_length line 171
  15. lemma OAI.Thomason.NormalizedChains.homTotal_bracket_supportedOn_lower line 184
  16. lemma OAI.Thomason.NormalizedChains.chains_eq_sum_bracket line 210
  17. lemma OAI.Thomason.NormalizedChains.append_positive line 220
  18. lemma OAI.Thomason.NormalizedChains.append_mem_grade line 223
  19. lemma OAI.Thomason.NormalizedChains.append_mem_supportedOn line 230
  20. lemma OAI.Thomason.NormalizedChains.append_append_self line 244
  21. lemma OAI.Thomason.NormalizedChains.boundary_append_supported line 254
  22. def OAI.Thomason.NormalizedChains.cutWord line 270
  23. lemma OAI.Thomason.NormalizedChains.cutWord_nil line 274
  24. lemma OAI.Thomason.NormalizedChains.cutWord_append line 279
  25. lemma OAI.Thomason.NormalizedChains.cutWord_of_all_zero line 284
  26. lemma OAI.Thomason.NormalizedChains.cutWord_positive line 290
  27. lemma OAI.Thomason.NormalizedChains.cutWord_grade line 300
  28. lemma OAI.Thomason.NormalizedChains.cutWord_supportedOn_lower line 310
  29. lemma OAI.Thomason.NormalizedChains.cutWord_boundary line 322
  30. lemma OAI.Thomason.NormalizedChains.cutWord_eq_zero_of_not_pairwise line 357
  31. def OAI.Thomason.NormalizedChains.cutTotal line 389
  32. lemma OAI.Thomason.NormalizedChains.cutTotal_bracket line 392
  33. lemma OAI.Thomason.NormalizedChains.cutTotal_grade line 401
  34. lemma OAI.Thomason.NormalizedChains.cutTotal_positive line 407
  35. lemma OAI.Thomason.NormalizedChains.cutTotal_wordBoundary line 411
  36. lemma OAI.Thomason.NormalizedChains.cutTotal_boundary line 421
  37. lemma OAI.Thomason.NormalizedChains.cutTotal_empty line 434
  38. lemma OAI.Thomason.NormalizedChains.cutTotal_augmentation line 438
  39. def OAI.Thomason.NormalizedChains.cutHom line 445
  40. lemma OAI.Thomason.NormalizedChains.homTotal_comp line 457
  41. lemma OAI.Thomason.NormalizedChains.homTotal_complexMap line 474
  42. lemma OAI.Thomason.NormalizedChains.homVertex_complexMap line 489
  43. lemma OAI.Thomason.NormalizedChains.homVertex_precomp line 495
  44. lemma OAI.Thomason.NormalizedChains.cutWord_precomp line 502
  45. lemma OAI.Thomason.NormalizedChains.cutTotal_precomp line 514
  46. lemma OAI.Thomason.NormalizedChains.cutHom_precomp line 529
  47. lemma OAI.Thomason.NormalizedChains.cutWord_const_one line 534
  48. lemma OAI.Thomason.NormalizedChains.cutTotal_const_zero line 542
  49. lemma OAI.Thomason.NormalizedChains.cutTotal_const_one line 553
  50. lemma OAI.Thomason.NormalizedChains.cutHom_const_zero line 565
  51. lemma OAI.Thomason.NormalizedChains.cutHom_const_one line 571
  52. def OAI.Thomason.tableNerveVertexMap line 588
  53. lemma OAI.Thomason.posetTableNerveMap_vertex line 601
  54. def OAI.Thomason.tableNerveCutSimplex line 613
  55. lemma OAI.Thomason.tableNerveCutSimplex_natural line 618
  56. def OAI.Thomason.tableNerveCutCylinder line 627
  57. def OAI.Thomason.tableNerveCutHomotopy line 637
  58. lemma OAI.Thomason.tableNerveVertexMap_weakEquivalence line 664
  59. lemma OAI.Thomason.posetTableNerveMap_weakEquivalence line 669
  60. lemma OAI.Thomason.posetCategorificationUnit_tableMap line 676
  61. theorem OAI.Thomason.posetCategorificationUnit_weakEquivalence line 681