OAI/Geometry/HyperbolicGroups/UniformMetricCover.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Uniform short exact lifts and uniform local metric preservation produce an actual topological covering, with no assumed covering-space producer.

  1. structure OAI.HyperbolicObstruction.UniformMetricCoverData line 15
  2. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.continuous line 24
  3. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.nearby_unique line 31
  4. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.discrete_fiber line 35
  5. abbrev OAI.HyperbolicObstruction.UniformMetricCoverData.U line 49
  6. abbrev OAI.HyperbolicObstruction.UniformMetricCoverData.F line 50
  7. abbrev OAI.HyperbolicObstruction.UniformMetricCoverData.V line 51
  8. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.recenter_exists line 53
  9. def OAI.HyperbolicObstruction.UniformMetricCoverData.recenter line 60
  10. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.recenter_dist line 61
  11. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.recenter_eq line 64
  12. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.recenter_continuous line 76
  13. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.out_exists line 83
  14. def OAI.HyperbolicObstruction.UniformMetricCoverData.out line 91
  15. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.out_proj line 93
  16. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.out_dist line 95
  17. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.out_isometry line 98
  18. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.out_recenter line 108
  19. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.recenter_out line 118
  20. def OAI.HyperbolicObstruction.UniformMetricCoverData.homeomorph line 128
  21. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.isCoveringMap line 138