OAI/GroupTheory/FiniteType/PresentationGeometry.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PresentationGeometry.quotientMk_isClosedMap line 11
  2. theorem OAI.PresentationGeometry.quotient_t2Space line 27
  3. def OAI.PresentationGeometry.Adjunction.normalize line 57
  4. def OAI.PresentationGeometry.Adjunction.relation line 61
  5. theorem OAI.PresentationGeometry.Adjunction.relation_iff line 64
  6. abbrev OAI.PresentationGeometry.Adjunction.Space line 67
  7. def OAI.PresentationGeometry.Adjunction.old line 69
  8. def OAI.PresentationGeometry.Adjunction.disk line 70
  9. theorem OAI.PresentationGeometry.Adjunction.normalize_inl line 72
  10. theorem OAI.PresentationGeometry.Adjunction.normalize_inr_mem line 75
  11. theorem OAI.PresentationGeometry.Adjunction.normalize_inr_notMem line 79
  12. theorem OAI.PresentationGeometry.Adjunction.relation_eq line 83
  13. theorem OAI.PresentationGeometry.Adjunction.relation_isClosed line 110
  14. theorem OAI.PresentationGeometry.Adjunction.t2Space line 125
  15. theorem OAI.PresentationGeometry.Adjunction.continuous_old line 129
  16. theorem OAI.PresentationGeometry.Adjunction.continuous_disk line 132
  17. theorem OAI.PresentationGeometry.Adjunction.old_inj line 135
  18. theorem OAI.PresentationGeometry.Adjunction.disk_boundary line 140
  19. theorem OAI.PresentationGeometry.Adjunction.old_isClosedEmbedding line 144
  20. def OAI.PresentationGeometry.Adjunction.interiorMap line 149
  21. theorem OAI.PresentationGeometry.Adjunction.disk_eq_disk_of_notMem line 151
  22. theorem OAI.PresentationGeometry.Adjunction.old_ne_disk_of_notMem line 162
  23. theorem OAI.PresentationGeometry.Adjunction.interiorMap_preimage_image line 168
  24. theorem OAI.PresentationGeometry.Adjunction.interiorMap_isOpenEmbedding line 180
  25. abbrev OAI.PresentationGeometry.Cells.Disk line 199
  26. abbrev OAI.PresentationGeometry.Cells.OpenDisk line 200
  27. def OAI.PresentationGeometry.Cells.boundary line 202
  28. theorem OAI.PresentationGeometry.Cells.boundary_closed line 205
  29. abbrev OAI.PresentationGeometry.Cells.Space line 211
  30. instance OAI.PresentationGeometry.Cells.(instance at line 213) line 213
  31. def OAI.PresentationGeometry.Cells.characteristic line 216
  32. theorem OAI.PresentationGeometry.Cells.characteristic_on_disk line 222
  33. theorem OAI.PresentationGeometry.Cells.characteristic_continuousOn line 226
  34. def OAI.PresentationGeometry.Cells.interiorInDisk line 236
  35. theorem OAI.PresentationGeometry.Cells.interiorInDisk_isOpenEmbedding line 238
  36. def OAI.PresentationGeometry.Cells.interiorInFamily line 241
  37. theorem OAI.PresentationGeometry.Cells.prodMk_isOpenEmbedding line 246
  38. theorem OAI.PresentationGeometry.Cells.interiorInFamily_isOpenEmbedding line 259
  39. theorem OAI.PresentationGeometry.Cells.characteristic_interior line 269
  40. theorem OAI.PresentationGeometry.Cells.characteristic_isOpenEmbedding line 275
  41. theorem OAI.PresentationGeometry.Cells.characteristic_injOn line 281
  42. def OAI.PresentationGeometry.Cells.chart line 287
  43. theorem OAI.PresentationGeometry.Cells.chart_coe line 290
  44. theorem OAI.PresentationGeometry.Cells.chart_source line 293
  45. theorem OAI.PresentationGeometry.Cells.chart_target line 295
  46. theorem OAI.PresentationGeometry.Cells.chart_continuousOn line 298
  47. theorem OAI.PresentationGeometry.Cells.chart_continuousOn_symm line 301
  48. def OAI.PresentationGeometry.Cells.oldChart line 310
  49. theorem OAI.PresentationGeometry.Cells.oldChart_apply line 316
  50. theorem OAI.PresentationGeometry.Cells.oldChart_source line 319
  51. theorem OAI.PresentationGeometry.Cells.oldChart_continuousOn line 323
  52. theorem OAI.PresentationGeometry.Cells.oldChart_continuousOn_symm line 327
  53. def OAI.PresentationGeometry.Cells.NewCell line 336
  54. def OAI.PresentationGeometry.Cells.newChart line 338
  55. theorem OAI.PresentationGeometry.Cells.newChart_old line 343
  56. theorem OAI.PresentationGeometry.Cells.newChart_new line 346
  57. theorem OAI.PresentationGeometry.Cells.newChart_source line 349
  58. theorem OAI.PresentationGeometry.Cells.newChart_continuousOn line 356
  59. theorem OAI.PresentationGeometry.Cells.newChart_continuousOn_symm line 364
  60. theorem OAI.PresentationGeometry.Cells.chart_apply_ball line 373
  61. theorem OAI.PresentationGeometry.Cells.chart_apply_sphere line 378
  62. theorem OAI.PresentationGeometry.Cells.newChart_cell_eq line 384
  63. theorem OAI.PresentationGeometry.Cells.newChart_pairwiseDisjoint line 422
  64. theorem OAI.PresentationGeometry.Cells.newChart_mapsTo line 433
  65. theorem OAI.PresentationGeometry.Cells.newChart_union line 459
  66. theorem OAI.PresentationGeometry.Cells.newCell_eventually_isEmpty line 478
  67. theorem OAI.PresentationGeometry.Cells.newCell_finite line 491
  68. def OAI.PresentationGeometry.Cells.cwComplex line 498
  69. theorem OAI.PresentationGeometry.Cells.cwComplex_finite line 504
  70. instance OAI.PresentationGeometry.Cells.disk_pathConnectedSpace line 513
  71. def OAI.PresentationGeometry.Cells.boundaryVector line 518
  72. theorem OAI.PresentationGeometry.Cells.boundaryVector_mem_sphere line 520
  73. theorem OAI.PresentationGeometry.Cells.pathConnectedSpace line 526
  74. abbrev OAI.PresentationGeometry.Rose.Point line 549
  75. instance OAI.PresentationGeometry.Rose.point_finiteType line 551
  76. theorem OAI.PresentationGeometry.Rose.point_dimension line 557
  77. def OAI.PresentationGeometry.Rose.attaching line 562
  78. abbrev OAI.PresentationGeometry.Rose.Space line 564
  79. instance OAI.PresentationGeometry.Rose.(instance at line 566) line 566
  80. instance OAI.PresentationGeometry.Rose.(instance at line 569) line 569
  81. instance OAI.PresentationGeometry.Rose.(instance at line 572) line 572
  82. theorem OAI.PresentationGeometry.Rose.dimension line 575
  83. def OAI.PresentationGeometry.Rose.basepoint line 582
  84. instance OAI.PresentationGeometry.Rose.(instance at line 584) line 584
  85. def OAI.PresentationGeometry.Rose.leftEnd line 586
  86. def OAI.PresentationGeometry.Rose.rightEnd line 587
  87. theorem OAI.PresentationGeometry.Rose.leftEnd_sphere line 589
  88. theorem OAI.PresentationGeometry.Rose.rightEnd_sphere line 593
  89. theorem OAI.PresentationGeometry.Rose.segmentInDisk line 597
  90. def OAI.PresentationGeometry.Rose.generatorLoop line 604
  91. def OAI.PresentationGeometry.Rose.letterLoop line 616
  92. def OAI.PresentationGeometry.Rose.wordLoop line 619
  93. def OAI.PresentationGeometry.Rose.freeToFundamental line 623
  94. theorem OAI.PresentationGeometry.Rose.freeToFundamental_mk line 626
  95. def OAI.PresentationGeometry.AttachingLoops.onCircle line 647
  96. abbrev OAI.PresentationGeometry.AttachingLoops.SquareBoundary line 653
  97. def OAI.PresentationGeometry.AttachingLoops.vectorComplex line 655
  98. theorem OAI.PresentationGeometry.AttachingLoops.vectorComplex_re line 657
  99. theorem OAI.PresentationGeometry.AttachingLoops.vectorComplex_im line 660
  100. theorem OAI.PresentationGeometry.AttachingLoops.vectorComplex_continuous line 663
  101. theorem OAI.PresentationGeometry.AttachingLoops.vectorComplex_ne_zero line 667
  102. def OAI.PresentationGeometry.AttachingLoops.boundaryAngle line 679
  103. def OAI.PresentationGeometry.AttachingLoops.boundaryParameter line 688
  104. def OAI.PresentationGeometry.AttachingLoops.complexVector line 692
  105. theorem OAI.PresentationGeometry.AttachingLoops.vectorComplex_complexVector line 694
  106. theorem OAI.PresentationGeometry.AttachingLoops.complexVector_continuous line 698
  107. theorem OAI.PresentationGeometry.AttachingLoops.complexVector_ne_zero line 705
  108. def OAI.PresentationGeometry.AttachingLoops.squareOfCircle line 712
  109. theorem OAI.PresentationGeometry.AttachingLoops.boundaryAngle_squareOfCircle line 720
  110. def OAI.PresentationGeometry.AttachingLoops.boundaryLift line 733
  111. theorem OAI.PresentationGeometry.AttachingLoops.boundaryParameter_boundaryLift line 739
  112. def OAI.PresentationGeometry.AttachingLoops.boundaryLoop line 749
  113. theorem OAI.PresentationGeometry.AttachingLoops.onCircle_coe line 758
  114. def OAI.PresentationGeometry.AttachingLoops.relators line 772
  115. abbrev OAI.PresentationGeometry.PresentationComplex.Space line 791
  116. instance OAI.PresentationGeometry.PresentationComplex.(instance at line 793) line 793
  117. instance OAI.PresentationGeometry.PresentationComplex.(instance at line 796) line 796
  118. instance OAI.PresentationGeometry.PresentationComplex.(instance at line 799) line 799
  119. theorem OAI.PresentationGeometry.PresentationComplex.dimension line 802
  120. def OAI.PresentationGeometry.PresentationComplex.basepoint line 809
  121. def OAI.PresentationGeometry.PresentationComplex.includeRose line 811
  122. def OAI.PresentationGeometry.PresentationComplex.freeToFundamental line 814
  123. def OAI.PresentationGeometry.PresentationComplex.diskMap line 817
  124. def OAI.PresentationGeometry.PresentationComplex.boundaryInDisk line 821
  125. theorem OAI.PresentationGeometry.PresentationComplex.diskMap_boundary line 825
  126. theorem OAI.PresentationGeometry.PresentationComplex.diskMap_boundary_basepoint line 831
  127. def OAI.PresentationGeometry.PresentationComplex.filledRelatorLoop line 838
  128. theorem OAI.PresentationGeometry.PresentationComplex.filledRelatorLoop_eq line 843
  129. theorem OAI.PresentationGeometry.PresentationComplex.relator_nullhomotopic line 851
  130. theorem OAI.PresentationGeometry.PresentationComplex.freeToFundamental_relator line 871
  131. def OAI.PresentationGeometry.PresentationComplex.relatorSet line 878
  132. def OAI.PresentationGeometry.PresentationComplex.presentedToFundamental line 880
  133. theorem OAI.PresentationGeometry.PresentationComplex.presentedToFundamental_mk line 888
  134. def OAI.PresentationGeometry.PresentationComplex.PresentationTheoremObligation line 892