OAI/Geometry/Cannon/Conformal/BoundedCrossRatios.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonMetricQC.weakQS_ae_complexLinear_holomorphic line 18
  2. theorem OAI.CannonMetricQC.weakQS_ae_conformal_rigidity line 41
  3. lemma OAI.CannonMetricQC.holomorphic_weakQS_inverse line 78
  4. lemma OAI.CannonMetricQC.WeakQS.post_conj line 102
  5. lemma OAI.CannonMetricQC.WeakQS.pre_conj line 108
  6. theorem OAI.CannonMetricQC.weakQS_ae_conformal_affine_or_anti line 113
  7. lemma OAI.CannonMetricQC.WeakQS.dyadic line 139
  8. lemma OAI.CannonMetricQC.WeakQS.bounded_ratios line 157
  9. theorem OAI.CannonMetricQC.WeakQS.crossRatio_bound line 164
  10. def OAI.CannonQM.BoundedCrossRatios line 201
  11. lemma OAI.CannonQM.BoundedCrossRatios.comp line 205
  12. lemma OAI.CannonQM.Controlled.boundedCrossRatios line 213
  13. lemma OAI.CannonQM.isOpen_distinct_quad line 224
  14. lemma OAI.CannonQM.boundedCrossRatios_dense line 232
  15. theorem OAI.CannonMobius.weakQS_sphere_boundedCrossRatios line 289
  16. lemma OAI.CannonMobius.boundedCrossRatios_restriction line 308