OAI/Geometry/Cannon/Conformal/Chart.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonStereo.stereo_inner line 14
  2. lemma OAI.CannonStereo.stereo_dist_sq line 27
  3. lemma OAI.CannonStereo.stereo_dist line 41
  4. lemma OAI.CannonMobius.coe_dist_sq line 61
  5. lemma OAI.CannonMobius.coe_dist_le line 66
  6. lemma OAI.CannonMobius.isometry_of_punctured_dist line 75
  7. def OAI.CannonMobius.chartZero line 95
  8. def OAI.CannonMobius.chartOne line 96
  9. lemma OAI.CannonMobius.chartZero_finite line 98
  10. lemma OAI.CannonMobius.chartOne_finite line 103
  11. lemma OAI.CannonMobius.chartOne_norm_id line 113
  12. theorem OAI.CannonMobius.chartZero_isometry line 120
  13. theorem OAI.CannonMobius.chartOne_isometry line 134