OAI/Geometry/NilpotentCharts/SubspaceQuotients.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth simply connected quotients by central vector subspaces.

  1. lemma OAI.RawLieIntegration.exists_subspace_quotient_injective_neighbourhood line 22
  2. lemma OAI.RawLieIntegration.subspace_quotient_productSlice line 64
  3. theorem OAI.RawLieIntegration.exists_subspace_quotient_openChart line 85
  4. lemma OAI.RawLieIntegration.subspace_quotient_coordinates_smooth line 141
  5. theorem OAI.RawLieIntegration.exists_subspace_quotient_smoothChart line 199
  6. theorem OAI.RawLieIntegration.exists_subspace_quotient_submersion line 229
  7. lemma OAI.RawLieIntegration.subspace_range_pathConnectedSpace line 251
  8. lemma OAI.RawLieIntegration.subspace_quotient_simplyConnected line 260