OAI/Combinatorics/Coboundary/Cones.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Quantitative chain cones, face-model transport, relabeling, and exactness under retractions.

  1. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.twice line 19
  2. def OAI.CoboundaryExpanders.InfiniteChains.Cone.size line 23
  3. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.size_zero line 26
  4. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.size_add_le line 28
  5. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.size_smul_le line 32
  6. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.size_single_le line 36
  7. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.size_sum_le line 39
  8. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.size_map_le line 44
  9. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.size_rawCone_le line 60
  10. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.rawCone_supported line 68
  11. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.rawCone_graded line 78
  12. def OAI.CoboundaryExpanders.InfiniteChains.Cone.carrierFill line 86
  13. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.carrierFill_eq line 91
  14. def OAI.CoboundaryExpanders.InfiniteChains.Cone.carrierMap line 98
  15. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.carrierMap_single line 101
  16. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.boundary_carrierFill line 105
  17. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.carrierMap_contraction line 131
  18. def OAI.CoboundaryExpanders.InfiniteChains.Cone.carrierBound line 145
  19. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.carrierFill_size line 149
  20. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.carrierFill_supported line 173
  21. def OAI.CoboundaryExpanders.InfiniteChains.Cone.link line 200
  22. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.link_single line 204
  23. def OAI.CoboundaryExpanders.InfiniteChains.Cone.without line 209
  24. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.without_single line 213
  25. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.cone_link_without line 217
  26. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.link_boundary line 231
  27. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.link_cycle line 252
  28. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.link_supported line 257
  29. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.link_graded line 267
  30. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.without_supported line 275
  31. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.link_size line 285
  32. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.without_size line 293
  33. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.elimination_identity line 301
  34. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.elimination_cycle line 317
  35. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.boundary_single_size line 324
  36. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.linear_eq_on_supported line 334
  37. structure OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone line 345
  38. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.map_graded line 357
  39. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.contraction_apply line 368
  40. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.size_apply line 377
  41. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.fills line 382
  42. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.exactIn line 388
  43. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.newCycle_supported line 392
  44. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.newCycle_cycle line 401
  45. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.newCycle_size line 411
  46. def OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.extend line 420
  47. def OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.initial line 483
  48. def OAI.CoboundaryExpanders.InfiniteChains.Cone.vertices line 501
  49. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.mem_vertices line 503
  50. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.vertices_card_le line 506
  51. def OAI.CoboundaryExpanders.InfiniteChains.Cone.allowed line 515
  52. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.allowed_forget line 521
  53. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.removeBad line 525
  54. def OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel line 582
  55. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_single line 586
  56. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_size line 591
  57. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_supported line 597
  58. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_graded line 606
  59. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_injective line 616
  60. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_boundary line 620
  61. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_comp line 633
  62. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_id line 641
  63. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_retraction line 648
  64. def OAI.CoboundaryExpanders.InfiniteChains.Cone.unlabel line 670
  65. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.unlabel_single line 674
  66. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.preimage_image line 679
  67. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.unlabel_relabel line 685
  68. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.unlabel_size line 697
  69. structure OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel line 703
  70. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.relabel_supported line 713
  71. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.unlabel_face line 718
  72. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.unlabel_graded line 727
  73. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.relabel_unlabel line 736
  74. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.unlabel_boundary line 744
  75. def OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.pullCone line 760
  76. def OAI.CoboundaryExpanders.InfiniteChains.Cone.FaceModel.pushCone line 794
  77. def OAI.CoboundaryExpanders.InfiniteChains.Cone.VertexPath line 842
  78. def OAI.CoboundaryExpanders.InfiniteChains.Cone.vertexEval line 845
  79. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.vertexEval_single line 848
  80. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.vertexEval_boundary line 852
  81. theorem OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.vertexPath line 880
  82. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.exactIn_equivalence line 916
  83. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.image_erase_of_injOn line 937
  84. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.relabel_boundary_on line 949
  85. theorem OAI.CoboundaryExpanders.InfiniteChains.Cone.exactIn_retract line 962
  86. def OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.retract line 976
  87. theorem OAI.CoboundaryExpanders.InfiniteChains.Cone.relativeExactIn_retract line 1007
  88. def OAI.CoboundaryExpanders.InfiniteChains.Cone.tagBy line 1035
  89. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.untag_tagBy line 1036
  90. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.tagBy_injective line 1038
  91. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.tagBy_left line 1042
  92. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.tagBy_right line 1053
  93. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.untag_image line 1064
  94. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.exactIn_of_image line 1078