OAI/Geometry/NilpotentCharts/QuotientCharts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Smooth central quotient charts, covering maps and central homeomorphisms.

  1. lemma OAI.RawLieIntegration.exists_smooth_localChart_of_derivative line 23
  2. theorem OAI.RawLieIntegration.exists_productSlice_partialDiffeomorph line 57
  3. lemma OAI.RawLieIntegration.quotient_coordinates_smooth line 76
  4. theorem OAI.RawLieIntegration.exists_central_quotient_smoothChart line 134
  5. instance OAI.RawLieIntegration.centralAxesHom_range_normal line 162
  6. lemma OAI.RawLieIntegration.central_quotient_t2Space line 167
  7. theorem OAI.RawLieIntegration.exists_central_quotient_lieChart line 174
  8. lemma OAI.RawLieIntegration.centralAxesHom_range_pathConnectedSpace line 202
  9. theorem OAI.RawLieIntegration.central_quotient_simplyConnected line 212
  10. lemma OAI.RawLieIntegration.centralAxes_range_continuous line 235
  11. lemma OAI.RawLieIntegration.centralAxes_range_isOpenMap line 237
  12. lemma OAI.RawLieIntegration.centralAxes_range_ker_discrete line 244
  13. lemma OAI.RawLieIntegration.centralAxes_range_covering line 266
  14. lemma OAI.RawLieIntegration.centralAxes_range_locallyPathConnected line 271
  15. lemma OAI.RawLieIntegration.centralAxes_injective line 278
  16. theorem OAI.RawLieIntegration.exists_central_quotient_submersion line 303
  17. def OAI.RawLieIntegration.centralHomeomorph line 326