OAI/Geometry/NilpotentCharts/QuotientLie.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Lie-group structures and surjective derivatives for quotient charts.

  1. def OAI.RawQuotientLie.leftChart line 18
  2. lemma OAI.RawQuotientLie.leftChart_apply line 22
  3. lemma OAI.RawQuotientLie.leftChart_symm_apply line 26
  4. lemma OAI.RawQuotientLie.leftChart_source line 32
  5. lemma OAI.RawQuotientLie.leftChart_target line 38
  6. def OAI.RawQuotientLie.quotientChartedSpace line 44
  7. lemma OAI.RawQuotientLie.quotient_isManifold line 51
  8. lemma OAI.RawQuotientLie.quotient_extChart_apply line 90
  9. lemma OAI.RawQuotientLie.quotient_extChart_symm_apply line 93
  10. lemma OAI.RawQuotientLie.quotient_projection_smooth line 98
  11. lemma OAI.RawQuotientLie.quotient_descend_smooth line 120
  12. lemma OAI.RawQuotientLie.quotient_multiplication_smooth line 138
  13. theorem OAI.RawQuotientLie.quotient_lieGroup line 168
  14. lemma OAI.RawQuotientLie.quotient_derivative_surjective line 192