OAI/CategoryTheory/Thomason/AlexanderWhitney.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Alexander Whitney.

  1. lemma OAI.Thomason.NormalizedChains.awZeroWord_map line 16
  2. lemma OAI.Thomason.NormalizedChains.awEdgeWord_map line 28
  3. lemma OAI.Thomason.NormalizedChains.awZero_map line 41
  4. lemma OAI.Thomason.NormalizedChains.awEdge_map line 58
  5. lemma OAI.Thomason.NormalizedChains.awHom_naturality line 77
  6. lemma OAI.Thomason.NormalizedChains.awHom_projection line 98
  7. lemma OAI.Thomason.NormalizedChains.awZero_const_zero line 105
  8. lemma OAI.Thomason.NormalizedChains.awEdge_const_zero line 118
  9. lemma OAI.Thomason.NormalizedChains.awZero_const_one_of_grade line 126
  10. lemma OAI.Thomason.NormalizedChains.awEdge_const_one_of_grade line 139
  11. lemma OAI.Thomason.NormalizedChains.awHom_endpoint line 160
  12. def OAI.Thomason.NormalizedChains.supportedOn line 200
  13. lemma OAI.Thomason.NormalizedChains.mem_supportedOn_iff line 203
  14. lemma OAI.Thomason.NormalizedChains.bracket_mem_supportedOn line 208
  15. lemma OAI.Thomason.NormalizedChains.faces_mem_submodule line 217
  16. lemma OAI.Thomason.NormalizedChains.wordBoundary_mem_supportedOn line 230
  17. lemma OAI.Thomason.NormalizedChains.boundary_mem_supportedOn line 237
  18. lemma OAI.Thomason.NormalizedChains.bracket_apply line 247
  19. lemma OAI.Thomason.NormalizedChains.prepend_apply_zero line 260
  20. def OAI.Thomason.NormalizedChains.tailWord line 269
  21. lemma OAI.Thomason.NormalizedChains.wordBoundary_leading line 283
  22. lemma OAI.Thomason.NormalizedChains.wordBoundary_leading' line 294
  23. lemma OAI.Thomason.NormalizedChains.tailWord_not_supported line 308
  24. lemma OAI.Thomason.NormalizedChains.positive_supportedOn_of_boundary line 327
  25. def OAI.Thomason.NormalizedChains.subsetWordEmbedding line 384
  26. lemma OAI.Thomason.NormalizedChains.mem_range_subsetWordEmbedding line 387
  27. def OAI.Thomason.NormalizedChains.restrictChain line 398
  28. lemma OAI.Thomason.NormalizedChains.restrictChain_apply line 401
  29. lemma OAI.Thomason.NormalizedChains.map_restrictChain line 404
  30. lemma OAI.Thomason.NormalizedChains.restrictChain_mem_grade line 413
  31. lemma OAI.Thomason.NormalizedChains.restrictChain_positive line 421
  32. lemma OAI.Thomason.NormalizedChains.map_mem_supportedOn line 424
  33. def OAI.Thomason.NormalizedChains.restrictGrade line 437
  34. lemma OAI.Thomason.NormalizedChains.complexMap_restrictGrade line 443
  35. def OAI.Thomason.NormalizedChains.restrictTable line 450
  36. lemma OAI.Thomason.NormalizedChains.table_map_restrictTable line 470
  37. lemma OAI.Thomason.NormalizedChains.table_map_orderEmbedding_injective line 476
  38. lemma OAI.Thomason.NormalizedChains.table_supportedOn_lower line 496
  39. lemma OAI.Thomason.NormalizedChains.table_initial_segment_unique_lift line 510
  40. def OAI.Thomason.NormalizedChains.reverseWord line 532
  41. def OAI.Thomason.NormalizedChains.reverseChain line 538
  42. lemma OAI.Thomason.NormalizedChains.reverseChain_apply line 540
  43. lemma OAI.Thomason.NormalizedChains.reverseChain_bracket line 543
  44. lemma OAI.Thomason.NormalizedChains.reverseChain_mem_grade line 557
  45. lemma OAI.Thomason.NormalizedChains.reverseChain_positive line 565
  46. lemma OAI.Thomason.NormalizedChains.reverseChain_supportedOn line 568
  47. lemma OAI.Thomason.NormalizedChains.supportedOn_of_reverseChain line 575
  48. lemma OAI.Thomason.NormalizedChains.faces_reverse line 587
  49. lemma OAI.Thomason.NormalizedChains.wordBoundary_reverse line 599
  50. lemma OAI.Thomason.NormalizedChains.boundary_reverseChain line 615
  51. lemma OAI.Thomason.NormalizedChains.positive_supportedOn_of_boundary_upper line 647
  52. lemma OAI.Thomason.NormalizedChains.table_supportedOn_upper line 658
  53. lemma OAI.Thomason.NormalizedChains.table_final_segment_unique_lift line 673
  54. lemma OAI.Thomason.NormalizedChains.augmentation_eq_sum line 695
  55. lemma OAI.Thomason.NormalizedChains.positive_mass_one line 706
  56. lemma OAI.Thomason.NormalizedChains.positive_augmentation_one line 733
  57. lemma OAI.Thomason.NormalizedChains.table_zero_row_vertex line 748
  58. def OAI.Thomason.NormalizedChains.vertexTable line 752
  59. lemma OAI.Thomason.NormalizedChains.vertexTable_row_zero line 775
  60. lemma OAI.Thomason.NormalizedChains.vertexTable_row_pos line 780
  61. lemma OAI.Thomason.NormalizedChains.vertexTable_source line 783
  62. lemma OAI.Thomason.NormalizedChains.bracket_singleton_injective line 789
  63. def OAI.Thomason.NormalizedChains.tableObjectsEquiv line 797