OAI/Geometry/Cannon/Actions/Proper.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Properness and cocompactness transferred through equivariant maps.

  1. def OAI.CannonActions.Proper line 23
  2. def OAI.CannonActions.Cocompact line 26
  3. theorem OAI.CannonActions.proper_descends line 29
  4. theorem OAI.CannonActions.cocompact_descends line 38
  5. theorem OAI.CannonActions.proper_finite_kernel line 48
  6. def OAI.CannonActions.conjugate line 56
  7. lemma OAI.CannonActions.conjugate_equivariant line 65
  8. theorem OAI.CannonActions.proper_conjugate line 70
  9. theorem OAI.CannonActions.cocompact_conjugate line 74
  10. abbrev OAI.CannonActions.OrderedTriples line 84
  11. def OAI.CannonActions.triplesMap line 85
  12. lemma OAI.CannonActions.continuous_triplesMap line 87
  13. def OAI.CannonActions.triplesCongr line 92
  14. def OAI.CannonActions.triplesHom line 100
  15. def OAI.CannonActions.triplesAction line 105
  16. lemma OAI.CannonActions.triples_conjugate line 107