OAI/Geometry/Cannon/Conformal/Distinct.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonQM.Distinct line 15
  2. lemma OAI.CannonQM.Distinct.map line 18
  3. lemma OAI.CannonQM.Distinct.flip line 24
  4. lemma OAI.CannonQM.nndist_pos line 28
  5. def OAI.CannonQM.crossRatio line 31
  6. lemma OAI.CannonQM.crossRatio_pos line 34
  7. lemma OAI.CannonQM.crossRatio_flip line 39
  8. abbrev OAI.CannonQM.Distortion line 43
  9. lemma OAI.CannonQM.distortion_zero line 45
  10. def OAI.CannonQM.reciprocal line 47
  11. def OAI.CannonQM.Controlled line 73
  12. def OAI.CannonQM.QuasiMobius line 77
  13. lemma OAI.CannonQM.Controlled.comp line 79
  14. lemma OAI.CannonQM.Controlled.inverse line 85
  15. lemma OAI.CannonQM.QuasiMobius.inverse line 100
  16. lemma OAI.CannonQM.QuasiMobius.comp line 104
  17. lemma OAI.CannonQM.controlled_conjugates line 110
  18. lemma OAI.CannonQM.controlled_of_product_bound line 125
  19. lemma OAI.CannonMetricQC.cycle_sorted_bounds line 147
  20. lemma OAI.CannonMetricQC.crossRatio_pair_bounds line 171