OAI/CategoryTheory/Thomason/NormalizedChains.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Normalized Chains.

  1. lemma OAI.Thomason.NormalizedChains.bracket_of_pairwise line 18
  2. lemma OAI.Thomason.NormalizedChains.bracket_of_not_pairwise line 23
  3. def OAI.Thomason.NormalizedChains.append line 29
  4. lemma OAI.Thomason.NormalizedChains.prepend_bracket line 32
  5. lemma OAI.Thomason.NormalizedChains.append_bracket line 44
  6. lemma OAI.Thomason.NormalizedChains.prepend_prepend_self line 58
  7. lemma OAI.Thomason.NormalizedChains.prepend_append line 72
  8. lemma OAI.Thomason.NormalizedChains.wordBoundary_nil line 87
  9. lemma OAI.Thomason.NormalizedChains.wordBoundary_cons line 88
  10. lemma OAI.Thomason.NormalizedChains.wordBoundary_repeated line 92
  11. lemma OAI.Thomason.NormalizedChains.wordBoundary_eq_zero_of_not_pairwise line 96
  12. lemma OAI.Thomason.NormalizedChains.boundary_bracket line 114
  13. lemma OAI.Thomason.NormalizedChains.faces_nil line 132
  14. lemma OAI.Thomason.NormalizedChains.faces_cons line 133
  15. lemma OAI.Thomason.NormalizedChains.faces_sub line 136
  16. lemma OAI.Thomason.NormalizedChains.faces_hom line 142
  17. lemma OAI.Thomason.NormalizedChains.faces_congr line 149
  18. lemma OAI.Thomason.NormalizedChains.faces_faces line 158
  19. lemma OAI.Thomason.NormalizedChains.faces_map line 167
  20. lemma OAI.Thomason.NormalizedChains.faces_append_singleton line 173
  21. lemma OAI.Thomason.NormalizedChains.faces_bracket line 185
  22. lemma OAI.Thomason.NormalizedChains.wordBoundary_append line 194
  23. lemma OAI.Thomason.NormalizedChains.boundary_wordBoundary line 202
  24. lemma OAI.Thomason.NormalizedChains.boundary_boundary line 217
  25. lemma OAI.Thomason.NormalizedChains.pairwise_of_map line 236
  26. lemma OAI.Thomason.NormalizedChains.map_bracket line 242
  27. lemma OAI.Thomason.NormalizedChains.map_wordBoundary line 254
  28. lemma OAI.Thomason.NormalizedChains.map_boundary line 263
  29. lemma OAI.Thomason.NormalizedChains.map_id line 280
  30. lemma OAI.Thomason.NormalizedChains.map_comp line 293
  31. def OAI.Thomason.NormalizedChains.prismWord line 313
  32. lemma OAI.Thomason.NormalizedChains.prismWord_nil line 317
  33. lemma OAI.Thomason.NormalizedChains.prismWord_append line 319
  34. lemma OAI.Thomason.NormalizedChains.prismWord_faces_append line 325
  35. lemma OAI.Thomason.NormalizedChains.prism_boundary_residual line 340
  36. lemma OAI.Thomason.NormalizedChains.bracket_repeat_end line 355
  37. def OAI.Thomason.NormalizedChains.prism line 363
  38. lemma OAI.Thomason.NormalizedChains.prismWord_eq_zero_of_not_pairwise line 366
  39. lemma OAI.Thomason.NormalizedChains.prism_bracket line 380
  40. lemma OAI.Thomason.NormalizedChains.prism_wordBoundary line 391
  41. lemma OAI.Thomason.NormalizedChains.prismWord_map line 402
  42. lemma OAI.Thomason.NormalizedChains.prism_map line 410
  43. def OAI.Thomason.NormalizedChains.degreeSign line 430
  44. lemma OAI.Thomason.NormalizedChains.degreeSign_bracket line 434
  45. lemma OAI.Thomason.NormalizedChains.bracket_positive line 447
  46. lemma OAI.Thomason.NormalizedChains.linearCombination_positive line 455
  47. lemma OAI.Thomason.NormalizedChains.map_positive line 466
  48. lemma OAI.Thomason.NormalizedChains.prismWord_positive line 470
  49. lemma OAI.Thomason.NormalizedChains.prism_positive line 476
  50. lemma OAI.Thomason.NormalizedChains.bracket_mem_grade line 481
  51. lemma OAI.Thomason.NormalizedChains.mem_grade_iff line 489
  52. lemma OAI.Thomason.NormalizedChains.linearCombination_mem_grade line 494
  53. lemma OAI.Thomason.NormalizedChains.map_mem_grade line 505
  54. lemma OAI.Thomason.NormalizedChains.prepend_mem_grade line 511
  55. lemma OAI.Thomason.NormalizedChains.wordBoundary_mem_grade line 517
  56. lemma OAI.Thomason.NormalizedChains.boundary_mem_grade line 529
  57. lemma OAI.Thomason.NormalizedChains.prismWord_mem_grade line 535
  58. lemma OAI.Thomason.NormalizedChains.prism_mem_grade line 543
  59. structure OAI.Thomason.RelativePrismData line 551
  60. lemma OAI.Thomason.RelativePrismData.prism_ordered line 565
  61. lemma OAI.Thomason.RelativePrismData.prism_cancellation line 579
  62. lemma OAI.Thomason.RelativePrismData.prism_boundary line 610
  63. lemma OAI.Thomason.RelativePrismData.prism_stationary line 619
  64. lemma OAI.Thomason.RelativePrismData.boundary_prism line 627