OAI/GroupTheory/PeriodicGroups/Frames/ExteriorComplex.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.Stability.Frames.Labels line 11
  2. abbrev OAI.SourceBurnside.Stability.Frames.Ambient line 12
  3. def OAI.SourceBurnside.Stability.Frames.vertex line 14
  4. def OAI.SourceBurnside.Stability.Frames.augmentation line 16
  5. def OAI.SourceBurnside.Stability.Frames.boundary line 18
  6. lemma OAI.SourceBurnside.Stability.Frames.augmentation_single line 22
  7. lemma OAI.SourceBurnside.Stability.Frames.boundary_vertex line 25
  8. lemma OAI.SourceBurnside.Stability.Frames.boundary_one line 28
  9. lemma OAI.SourceBurnside.Stability.Frames.boundary_boundary line 31
  10. lemma OAI.SourceBurnside.Stability.Frames.boundary_cone line 34
  11. def OAI.SourceBurnside.Stability.Frames.basis line 42
  12. lemma OAI.SourceBurnside.Stability.Frames.basis_empty line 44
  13. lemma OAI.SourceBurnside.Stability.Frames.basis_singleton line 48
  14. lemma OAI.SourceBurnside.Stability.Frames.vertex_mul_basis line 57
  15. def OAI.SourceBurnside.Stability.Frames.chains line 75
  16. lemma OAI.SourceBurnside.Stability.Frames.basis_mem_chains line 79
  17. lemma OAI.SourceBurnside.Stability.Frames.chains_mono line 83
  18. lemma OAI.SourceBurnside.Stability.Frames.cone_mem_chains line 89
  19. lemma OAI.SourceBurnside.Stability.Frames.boundary_basis_mem line 110
  20. lemma OAI.SourceBurnside.Stability.Frames.boundary_mem_chains line 144
  21. lemma OAI.SourceBurnside.Stability.Frames.vertex_mem_chains line 155
  22. lemma OAI.SourceBurnside.Stability.Frames.exists_outside_labels line 165
  23. structure OAI.SourceBurnside.Stability.Frames.ConeSupply line 180
  24. def OAI.SourceBurnside.Stability.Frames.coneSupply line 185
  25. def OAI.SourceBurnside.Stability.Frames.baseLabel line 198
  26. lemma OAI.SourceBurnside.Stability.Frames.baseLabel_ne_zero line 201
  27. def OAI.SourceBurnside.Stability.Frames.cone0 line 205
  28. def OAI.SourceBurnside.Stability.Frames.support0 line 207
  29. lemma OAI.SourceBurnside.Stability.Frames.subset_support0 line 209
  30. lemma OAI.SourceBurnside.Stability.Frames.support0_mono line 213
  31. lemma OAI.SourceBurnside.Stability.Frames.card_support0 line 216
  32. def OAI.SourceBurnside.Stability.Frames.homotopy0Vertex line 223
  33. lemma OAI.SourceBurnside.Stability.Frames.boundary_homotopy0Vertex line 226
  34. def OAI.SourceBurnside.Stability.Frames.homotopy0 line 230
  35. lemma OAI.SourceBurnside.Stability.Frames.homotopy0_vertex line 233
  36. lemma OAI.SourceBurnside.Stability.Frames.boundary_homotopy0 line 237
  37. lemma OAI.SourceBurnside.Stability.Frames.homotopy0Vertex_mem line 248
  38. lemma OAI.SourceBurnside.Stability.Frames.homotopy0_mem line 266
  39. def OAI.SourceBurnside.Stability.Frames.cone1 line 279
  40. def OAI.SourceBurnside.Stability.Frames.support1 line 281
  41. lemma OAI.SourceBurnside.Stability.Frames.subset_support1 line 284
  42. lemma OAI.SourceBurnside.Stability.Frames.small_support1 line 287
  43. def OAI.SourceBurnside.Stability.Frames.homotopy1Basis line 295
  44. def OAI.SourceBurnside.Stability.Frames.homotopy1 line 298
  45. lemma OAI.SourceBurnside.Stability.Frames.homotopy1_basis line 301
  46. lemma OAI.SourceBurnside.Stability.Frames.boundary_homotopy1Basis line 305
  47. lemma OAI.SourceBurnside.Stability.Frames.boundary_homotopy1 line 313
  48. lemma OAI.SourceBurnside.Stability.Frames.homotopy1Basis_mem line 324
  49. lemma OAI.SourceBurnside.Stability.Frames.homotopy1_mem line 338
  50. def OAI.SourceBurnside.Stability.Frames.cone2 line 354
  51. def OAI.SourceBurnside.Stability.Frames.homotopy2Basis line 356
  52. def OAI.SourceBurnside.Stability.Frames.homotopy2 line 359
  53. lemma OAI.SourceBurnside.Stability.Frames.homotopy2_basis line 362
  54. lemma OAI.SourceBurnside.Stability.Frames.boundary_homotopy2Basis line 366
  55. lemma OAI.SourceBurnside.Stability.Frames.boundary_homotopy2 line 374
  56. lemma OAI.SourceBurnside.Stability.Frames.homotopy2Basis_mem line 385
  57. lemma OAI.SourceBurnside.Stability.Frames.homotopy2_mem line 400
  58. theorem OAI.SourceBurnside.Stability.Frames.twoCycle_bounds line 411
  59. lemma OAI.SourceBurnside.Stability.Frames.homotopy0_mem_univ line 419
  60. lemma OAI.SourceBurnside.Stability.Frames.homotopy1_mem_univ line 431
  61. lemma OAI.SourceBurnside.Stability.Frames.degreeZero_support line 443
  62. lemma OAI.SourceBurnside.Stability.Frames.boundary_degreeZero line 455
  63. lemma OAI.SourceBurnside.Stability.Frames.degreeZero_lift line 468
  64. theorem OAI.SourceBurnside.Stability.Frames.cycles_bound_upToThree line 476
  65. def OAI.SourceBurnside.Stability.Frames.differential line 490
  66. lemma OAI.SourceBurnside.Stability.Frames.differential_val line 493
  67. lemma OAI.SourceBurnside.Stability.Frames.differential_sq line 496
  68. def OAI.SourceBurnside.Stability.Frames.augmentedComplex line 502
  69. lemma OAI.SourceBurnside.Stability.Frames.augmentedComplex_d line 507
  70. theorem OAI.SourceBurnside.Stability.Frames.augmentedComplex_exact line 514
  71. def OAI.SourceBurnside.Stability.Frames.labelMap line 547
  72. lemma OAI.SourceBurnside.Stability.Frames.labelMap_vertex line 550
  73. lemma OAI.SourceBurnside.Stability.Frames.labelMap_id line 554
  74. lemma OAI.SourceBurnside.Stability.Frames.labelMap_comp line 557
  75. lemma OAI.SourceBurnside.Stability.Frames.basis_insert_inverse line 562
  76. lemma OAI.SourceBurnside.Stability.Frames.labelMap_basis line 568
  77. lemma OAI.SourceBurnside.Stability.Frames.boundary_labelMap line 582
  78. def OAI.SourceBurnside.Stability.Frames.ambientAction line 598
  79. lemma OAI.SourceBurnside.Stability.Frames.labelMap_chains line 619
  80. def OAI.SourceBurnside.Stability.Frames.chainSubrepresentation line 637
  81. def OAI.SourceBurnside.Stability.Frames.chainRep line 641