OAI/Geometry/Cannon/Actions/Triples.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CannonTriples.Triples line 16
  2. instance OAI.CannonTriples.(instance at line 18) line 18
  3. def OAI.CannonTriples.separation line 23
  4. lemma OAI.CannonTriples.separation_pos line 25
  5. lemma OAI.CannonTriples.separation_le line 32
  6. lemma OAI.CannonTriples.injective_of_separation_pos line 48
  7. lemma OAI.CannonTriples.continuous_separation line 54
  8. theorem OAI.CannonTriples.compact_uniform_separation line 58
  9. theorem OAI.CannonTriples.separated_compact line 66
  10. def OAI.CannonTriples.map line 80
  11. lemma OAI.CannonTriples.map_continuous line 83
  12. def OAI.CannonTriples.homeomorph line 89
  13. theorem OAI.CannonRelease.boundary_triples_proper line 109
  14. theorem OAI.CannonRelease.boundary_triples_normalize line 140
  15. theorem OAI.CannonRelease.boundary_triples_cocompact line 174