OAI/Geometry/NilpotentCharts/QuotientTopology.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Path lifting, simple connectivity and topological group sections.

  1. theorem OAI.RawQuotientTopology.exists_path_lift line 19
  2. theorem OAI.RawQuotientTopology.simplyConnected_quotient line 83
  3. lemma OAI.RawQuotientTopology.local_sections_of_chart line 118
  4. theorem OAI.RawGroupSection.simplyConnected_retract line 141
  5. def OAI.RawGroupSection.fiberRetraction line 156
  6. lemma OAI.RawGroupSection.fiberRetraction_continuous line 161
  7. lemma OAI.RawGroupSection.fiberRetraction_leftInverse line 166
  8. theorem OAI.RawGroupSection.fiber_simplyConnected line 176
  9. def OAI.RawGroupSection.trivialization line 182
  10. def OAI.RawGroupSection.finAppendHomeomorph line 202