OAI/Geometry/ConjugatePoints/Gluing.lean

GitHub source file

163 declarations, 0 contain sorry, 0 declared as axioms

Two-piece gluing, smooth charts, compactness, and orientation.

  1. def OAI.ThreeManifold.TwoGluing.overlap line 39
  2. def OAI.ThreeManifold.TwoGluing.transition line 45
  3. lemma OAI.ThreeManifold.TwoGluing.transition_continuous line 53
  4. lemma OAI.ThreeManifold.TwoGluing.transition_inter line 57
  5. abbrev OAI.ThreeManifold.TwoGluing.datum line 62
  6. abbrev OAI.ThreeManifold.TwoGluing.Space line 80
  7. def OAI.ThreeManifold.TwoGluing.inclusion line 82
  8. lemma OAI.ThreeManifold.TwoGluing.inclusion_openEmbedding line 85
  9. lemma OAI.ThreeManifold.TwoGluing.inclusion_surjective line 88
  10. lemma OAI.ThreeManifold.TwoGluing.inclusion_mixed_eq line 91
  11. lemma OAI.ThreeManifold.TwoGluing.inclusion_transition line 100
  12. lemma OAI.ThreeManifold.TwoGluing.inclusion_symm_transition line 104
  13. lemma OAI.ThreeManifold.TwoGluing.space_connected line 108
  14. def OAI.ThreeManifold.TwoGluing.projection line 128
  15. lemma OAI.ThreeManifold.TwoGluing.projection_openQuotient line 131
  16. lemma OAI.ThreeManifold.TwoGluing.space_secondCountable line 139
  17. lemma OAI.ThreeManifold.TwoGluing.same_piece_separation line 143
  18. lemma OAI.ThreeManifold.TwoGluing.mixed_separation line 154
  19. lemma OAI.ThreeManifold.TwoGluing.space_t2 line 175
  20. lemma OAI.ThreeManifold.TwoGluing.space_compact line 189
  21. instance OAI.ThreeManifold.GluedConstruction.(instance at line 215) line 215
  22. abbrev OAI.ThreeManifold.GluedConstruction.Circle line 216
  23. abbrev OAI.ThreeManifold.GluedConstruction.Piece line 217
  24. instance OAI.ThreeManifold.GluedConstruction.(instance at line 218) line 218
  25. instance OAI.ThreeManifold.GluedConstruction.(instance at line 220) line 220
  26. instance OAI.ThreeManifold.GluedConstruction.(instance at line 223) line 223
  27. def OAI.ThreeManifold.GluedConstruction.collar line 227
  28. lemma OAI.ThreeManifold.GluedConstruction.collar_height line 230
  29. def OAI.ThreeManifold.GluedConstruction.collarCoordinates line 235
  30. lemma OAI.ThreeManifold.GluedConstruction.collarCoordinates_height line 281
  31. def OAI.ThreeManifold.GluedConstruction.collarFlip line 284
  32. def OAI.ThreeManifold.GluedConstruction.torusShear line 304
  33. def OAI.ThreeManifold.GluedConstruction.gluingMap line 312
  34. lemma OAI.ThreeManifold.GluedConstruction.gluing_height line 315
  35. lemma OAI.ThreeManifold.GluedConstruction.gluing_symm_height line 321
  36. abbrev OAI.ThreeManifold.GluedConstruction.Manifold line 329
  37. def OAI.ThreeManifold.GluedConstruction.inclusion line 331
  38. def OAI.ThreeManifold.GluedConstruction.halfCore line 333
  39. lemma OAI.ThreeManifold.GluedConstruction.halfCore_compact line 334
  40. lemma OAI.ThreeManifold.GluedConstruction.collar_nonempty line 341
  41. instance OAI.ThreeManifold.GluedConstruction.(instance at line 345) line 345
  42. instance OAI.ThreeManifold.GluedConstruction.(instance at line 346) line 346
  43. lemma OAI.ThreeManifold.GluedConstruction.halfCore_covers line 348
  44. lemma OAI.ThreeManifold.GluedConstruction.halfCore_covers_symm line 364
  45. instance OAI.ThreeManifold.GluedConstruction.(instance at line 380) line 380
  46. instance OAI.ThreeManifold.GluedConstruction.(instance at line 383) line 383
  47. abbrev OAI.ThreeManifold.CircleConstruction.Deck line 409
  48. lemma OAI.ThreeManifold.CircleConstruction.projection_cover line 410
  49. def OAI.ThreeManifold.CircleConstruction.sectionMap line 412
  50. lemma OAI.ThreeManifold.CircleConstruction.section_spec line 413
  51. lemma OAI.ThreeManifold.CircleConstruction.action_smooth line 415
  52. instance OAI.ThreeManifold.CircleConstruction.circleCharts line 419
  53. instance OAI.ThreeManifold.CircleConstruction.circleSmooth line 421
  54. lemma OAI.ThreeManifold.CircleConstruction.projection_smooth line 423
  55. def OAI.ThreeManifold.CircleConstruction.localLift line 425
  56. lemma OAI.ThreeManifold.CircleConstruction.localLift_source line 427
  57. lemma OAI.ThreeManifold.CircleConstruction.localLift_smooth line 432
  58. lemma OAI.ThreeManifold.CircleConstruction.localLift_right line 436
  59. lemma OAI.ThreeManifold.CircleConstruction.localLift_eventually line 439
  60. lemma OAI.ThreeManifold.CircleConstruction.addition_smooth line 444
  61. lemma OAI.ThreeManifold.CircleConstruction.negation_smooth line 459
  62. def OAI.ThreeManifold.HyperbolicCore.cuspOpens line 475
  63. instance OAI.ThreeManifold.HyperbolicCore.cuspCharts line 476
  64. instance OAI.ThreeManifold.HyperbolicCore.cuspSmooth line 478
  65. def OAI.ThreeManifold.HyperbolicCore.highOpens line 480
  66. instance OAI.ThreeManifold.HyperbolicCore.highCharts line 481
  67. instance OAI.ThreeManifold.HyperbolicCore.highSmooth line 483
  68. def OAI.ThreeManifold.HyperbolicCore.rayOpens line 485
  69. instance OAI.ThreeManifold.HyperbolicCore.rayCharts line 486
  70. instance OAI.ThreeManifold.HyperbolicCore.raySmooth line 488
  71. def OAI.ThreeManifold.HyperbolicCore.coreOpens line 490
  72. instance OAI.ThreeManifold.HyperbolicCore.coreCharts line 491
  73. instance OAI.ThreeManifold.HyperbolicCore.coreSmooth line 493
  74. lemma OAI.ThreeManifold.HyperbolicCore.upperHalfPlane_coe_real_smooth line 496
  75. lemma OAI.ThreeManifold.HyperbolicCore.upperHalfPlane_im_smooth line 503
  76. lemma OAI.ThreeManifold.HyperbolicCore.upperHalfPlane_re_smooth line 505
  77. lemma OAI.ThreeManifold.HyperbolicCore.upperHalfPlane_ofComplex_real_smoothAt line 508
  78. lemma OAI.ThreeManifold.HyperbolicCore.highProjection_smooth line 514
  79. lemma OAI.ThreeManifold.HyperbolicCore.highCylinderProjection_smooth line 519
  80. lemma OAI.ThreeManifold.HyperbolicCore.cuspCoordinates_smooth line 527
  81. lemma OAI.ThreeManifold.HyperbolicCore.cuspCoordinates_symm_smooth line 565
  82. def OAI.ThreeManifold.TwoGluing.extendedTransition line 617
  83. lemma OAI.ThreeManifold.TwoGluing.extendedTransition_apply line 621
  84. lemma OAI.ThreeManifold.TwoGluing.extendedTransition_smooth line 625
  85. def OAI.ThreeManifold.TwoGluing.pieceChart line 632
  86. def OAI.ThreeManifold.TwoGluing.representative line 635
  87. lemma OAI.ThreeManifold.TwoGluing.representative_spec line 638
  88. def OAI.ThreeManifold.TwoGluing.gluedCharts line 643
  89. lemma OAI.ThreeManifold.TwoGluing.pieceChart_apply line 651
  90. lemma OAI.ThreeManifold.TwoGluing.pieceChart_mixed_germ line 656
  91. lemma OAI.ThreeManifold.TwoGluing.pieceChart_mixed_symm_germ line 669
  92. lemma OAI.ThreeManifold.TwoGluing.same_chart_smooth line 681
  93. lemma OAI.ThreeManifold.TwoGluing.mixed_chart_smooth line 695
  94. lemma OAI.ThreeManifold.TwoGluing.mixed_symm_chart_smooth line 712
  95. lemma OAI.ThreeManifold.TwoGluing.glued_isManifold line 736
  96. abbrev OAI.ThreeManifold.GluedConstruction.IP line 761
  97. abbrev OAI.ThreeManifold.GluedConstruction.IT line 762
  98. abbrev OAI.ThreeManifold.GluedConstruction.IC line 763
  99. def OAI.ThreeManifold.GluedConstruction.bandOpens line 765
  100. instance OAI.ThreeManifold.GluedConstruction.bandCharts line 766
  101. instance OAI.ThreeManifold.GluedConstruction.bandSmooth line 768
  102. lemma OAI.ThreeManifold.GluedConstruction.collarCoordinates_smooth line 771
  103. lemma OAI.ThreeManifold.GluedConstruction.collarCoordinates_symm_smooth line 784
  104. lemma OAI.ThreeManifold.GluedConstruction.collarFlip_smooth line 798
  105. lemma OAI.ThreeManifold.GluedConstruction.collarFlip_symm_smooth line 804
  106. lemma OAI.ThreeManifold.GluedConstruction.torusShear_smooth line 807
  107. lemma OAI.ThreeManifold.GluedConstruction.torusShear_symm_smooth line 810
  108. lemma OAI.ThreeManifold.GluedConstruction.gluingMap_smooth line 817
  109. lemma OAI.ThreeManifold.GluedConstruction.gluingMap_symm_smooth line 822
  110. instance OAI.ThreeManifold.GluedConstruction.pieceSelfCharts line 827
  111. instance OAI.ThreeManifold.GluedConstruction.pieceSelfSmooth line 830
  112. instance OAI.ThreeManifold.GluedConstruction.manifoldCharts line 834
  113. instance OAI.ThreeManifold.GluedConstruction.manifoldSmooth line 837
  114. def OAI.ThreeManifold.AtlasOrientation.Positive line 853
  115. lemma OAI.ThreeManifold.AtlasOrientation.transition_contDiffAt line 858
  116. lemma OAI.ThreeManifold.AtlasOrientation.product line 865
  117. lemma OAI.ThreeManifold.AtlasOrientation.open_subset line 881
  118. lemma OAI.ThreeManifold.AtlasOrientation.transition_det_mul line 908
  119. lemma OAI.ThreeManifold.AtlasOrientation.reverse_positive line 933
  120. lemma OAI.ThreeManifold.QuotientConstruction.manifold_quotient_positive line 949
  121. lemma OAI.ThreeManifold.QuotientConstruction.manifold_projection_positive line 987
  122. lemma OAI.ThreeManifold.HyperbolicCore.action_orientation line 1018
  123. lemma OAI.ThreeManifold.HyperbolicCore.surface_positive line 1048
  124. lemma OAI.ThreeManifold.CircleConstruction.positive line 1058
  125. lemma OAI.ThreeManifold.GluedConstruction.piece_positive line 1067
  126. lemma OAI.ThreeManifold.HyperbolicCore.projection_chart_positive line 1075
  127. lemma OAI.ThreeManifold.CircleConstruction.projection_chart_positive line 1097
  128. def OAI.ThreeManifold.GluedConstruction.coverChart line 1110
  129. lemma OAI.ThreeManifold.GluedConstruction.coverChart_component_smooth line 1114
  130. lemma OAI.ThreeManifold.GluedConstruction.coverChart_positive line 1133
  131. lemma OAI.ThreeManifold.GluedConstruction.coverChart_smooth line 1148
  132. lemma OAI.ThreeManifold.GluedConstruction.coverChart_apply line 1155
  133. def OAI.ThreeManifold.GluedConstruction.neckLift line 1167
  134. lemma OAI.ThreeManifold.GluedConstruction.neckLift_coordinates line 1172
  135. lemma OAI.ThreeManifold.GluedConstruction.neckLift_surjective line 1180
  136. def OAI.ThreeManifold.GluedConstruction.flipUpper line 1193
  137. lemma OAI.ThreeManifold.GluedConstruction.flipUpper_im line 1195
  138. lemma OAI.ThreeManifold.GluedConstruction.flipUpper_re line 1198
  139. lemma OAI.ThreeManifold.GluedConstruction.flipUpper_band line 1201
  140. lemma OAI.ThreeManifold.GluedConstruction.neckLift_gluing line 1206
  141. lemma OAI.ThreeManifold.GluedConstruction.neckLift_chart line 1220
  142. lemma OAI.ThreeManifold.GluedConstruction.neckLift_chart_source line 1224
  143. def OAI.ThreeManifold.Coordinates3.coordinates line 1237
  144. def OAI.ThreeManifold.Coordinates3.shearD line 1245
  145. lemma OAI.ThreeManifold.Coordinates3.det_shearD line 1250
  146. def OAI.ThreeManifold.Coordinates3.liftedGluing line 1263
  147. lemma OAI.ThreeManifold.Coordinates3.liftedGluing_derivative line 1266
  148. lemma OAI.ThreeManifold.GluedConstruction.cover_transition_germ line 1286
  149. lemma OAI.ThreeManifold.GluedConstruction.gluing_transition_positive line 1325
  150. def OAI.ThreeManifold.Rechart.chart line 1389
  151. lemma OAI.ThreeManifold.Rechart.chart_source line 1393
  152. lemma OAI.ThreeManifold.Rechart.chart_target line 1396
  153. def OAI.ThreeManifold.Rechart.charts line 1404
  154. lemma OAI.ThreeManifold.Rechart.isManifold line 1412
  155. def OAI.ThreeManifold.Rechart.realThree line 1432
  156. lemma OAI.ThreeManifold.Rechart.positive line 1438
  157. lemma OAI.ThreeManifold.TwoGluing.mixed_chart_positive line 1464
  158. lemma OAI.ThreeManifold.TwoGluing.glued_positive line 1483
  159. lemma OAI.ThreeManifold.GluedConstruction.manifold_positive line 1531
  160. instance OAI.ThreeManifold.GluedConstruction.realCharts line 1537
  161. instance OAI.ThreeManifold.GluedConstruction.realSmooth line 1538
  162. lemma OAI.ThreeManifold.GluedConstruction.manifold_oriented line 1541
  163. theorem OAI.ThreeManifold.GluedConstruction.closed_oriented_candidate line 1544