OAI/GroupTheory/PolycyclicRecognition/Geometry/SemidirectProductTopology.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The product topology on the Cartan semidirect cover

  1. def OAI.PolycyclicRecognition.semidirectProductTopology line 17
  2. def OAI.PolycyclicRecognition.semidirectProductHomeomorph line 22
  3. theorem OAI.PolycyclicRecognition.continuous_semidirect_left line 27
  4. theorem OAI.PolycyclicRecognition.continuous_semidirect_right line 30
  5. theorem OAI.PolycyclicRecognition.continuous_semidirect_inl line 33
  6. theorem OAI.PolycyclicRecognition.continuous_semidirect_inr line 38
  7. instance OAI.PolycyclicRecognition.(instance at line 43) line 43
  8. instance OAI.PolycyclicRecognition.(instance at line 46) line 46
  9. instance OAI.PolycyclicRecognition.(instance at line 50) line 50
  10. instance OAI.PolycyclicRecognition.(instance at line 54) line 54
  11. theorem OAI.PolycyclicRecognition.semidirectProductTopologicalGroup line 60
  12. def OAI.PolycyclicRecognition.semidirectProductLift line 76
  13. theorem OAI.PolycyclicRecognition.continuous_semidirect_lift line 81