OAI/Geometry/Cannon/Conformal/PreservesProducts.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonRelease.boundary_quasiMobius_uniformizer line 16
  2. lemma OAI.CannonStereo.stereo_crossRatio line 54
  3. lemma OAI.CannonMobius.coe_dist line 83
  4. lemma OAI.CannonMobius.coe_crossRatio line 88
  5. lemma OAI.CannonMobius.roundChart_crossRatio line 96
  6. def OAI.CannonMobius.PreservesProducts line 107
  7. lemma OAI.CannonMobius.preservesProducts_dense line 111
  8. lemma OAI.CannonMobius.PreservesProducts.crossRatio line 128
  9. lemma OAI.CannonMobius.PreservesProducts.controlled line 141
  10. lemma OAI.CannonMobius.inversion_preservesProducts line 145
  11. lemma OAI.CannonMobius.affine_preservesProducts line 157
  12. lemma OAI.CannonMobius.inversion_controlled line 168
  13. lemma OAI.CannonMobius.affine_controlled line 170
  14. def OAI.CannonMetricQC.WeakQS line 183
  15. lemma OAI.CannonQM.eventually_dist_large line 190
  16. theorem OAI.CannonQM.Controlled.plane_weakQS line 197
  17. def OAI.CannonMobius.sendToInfty line 264
  18. lemma OAI.CannonMobius.sendToInfty_apply line 268
  19. lemma OAI.CannonMobius.sendToInfty_controlled line 275
  20. lemma OAI.CannonMobius.restriction_controlled line 284
  21. theorem OAI.CannonMobius.normalized_weakQS line 294
  22. def OAI.CannonMetricQC.DensityOne line 323
  23. theorem OAI.CannonMetricQC.DensityOne.approximate line 327
  24. theorem OAI.CannonMetricQC.derivative_of_density line 400
  25. def OAI.CannonMetricQC.PointwiseLip line 466
  26. def OAI.CannonMetricQC.lipPiece line 469
  27. lemma OAI.CannonMetricQC.lipPiece_closed line 473
  28. lemma OAI.CannonMetricQC.lipPiece_lipschitz line 491
  29. lemma OAI.CannonMetricQC.PointwiseLip.mem_lipPiece line 512
  30. theorem OAI.CannonMetricQC.continuous_ae_differentiable_of_pointwiseLip line 530