OAI/Geometry/Cannon/Conformal/Sphere.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CannonMobius.Sphere line 13
  2. def OAI.CannonMobius.inv line 15
  3. lemma OAI.CannonMobius.inv_infty line 18
  4. lemma OAI.CannonMobius.inv_zero line 19
  5. lemma OAI.CannonMobius.inv_coe line 20
  6. lemma OAI.CannonMobius.inv_involutive line 22
  7. lemma OAI.CannonMobius.continuous_inv line 31
  8. def OAI.CannonMobius.inversion line 62
  9. def OAI.CannonMobius.sphereHomeomorph line 70
  10. lemma OAI.CannonConformal.homeomorph_tendsto_cobounded line 80
  11. def OAI.CannonConformal.inverted line 84
  12. lemma OAI.CannonConformal.inverted_zero line 86
  13. lemma OAI.CannonConformal.inverted_continuousAt_zero line 89
  14. lemma OAI.CannonConformal.inverted_differentiable line 97
  15. lemma OAI.CannonConformal.inverted_leftInverse line 113
  16. theorem OAI.CannonConformal.biholomorphic_fix_zero_linear line 118
  17. theorem OAI.CannonConformal.biholomorphic_affine line 168
  18. def OAI.CannonMobius.coordinate line 190
  19. lemma OAI.CannonMobius.coordinate_coe line 191
  20. lemma OAI.CannonMobius.coordinate_infty line 192
  21. lemma OAI.CannonMobius.coe_coordinate line 193
  22. lemma OAI.CannonMobius.continuousAt_coordinate line 198
  23. lemma OAI.CannonMobius.coe_map_ne_infty line 203
  24. lemma OAI.CannonMobius.symm_infty line 206
  25. def OAI.CannonMobius.finiteRestriction line 210
  26. lemma OAI.CannonMobius.restriction_extension line 228
  27. def OAI.CannonMobius.chart line 236
  28. lemma OAI.CannonMobius.chart_involutive line 240
  29. lemma OAI.CannonMobius.coordinate_inv_coe line 245
  30. def OAI.CannonMobius.inChart line 250
  31. def OAI.CannonMobius.chartDomain line 252
  32. lemma OAI.CannonMobius.isOpen_chartDomain line 255
  33. def OAI.CannonMobius.IsAnalytic line 259
  34. lemma OAI.CannonMobius.analytic_differentiableAt line 262
  35. lemma OAI.CannonMobius.isAnalytic_mul line 267
  36. lemma OAI.CannonMobius.restriction_differentiable line 298
  37. lemma OAI.CannonMobius.restriction_symm line 303
  38. theorem OAI.CannonMobius.analytic_fix_infty_affine line 306
  39. abbrev OAI.CannonSphereReflection.S line 327
  40. def OAI.CannonSphereReflection.reflection line 329
  41. lemma OAI.CannonSphereReflection.reflection_infty line 332
  42. lemma OAI.CannonSphereReflection.reflection_zero line 335
  43. lemma OAI.CannonSphereReflection.reflection_coe line 338
  44. lemma OAI.CannonSphereReflection.reflection_fix line 343
  45. lemma OAI.CannonSphereReflection.reflection_involutive line 349
  46. lemma OAI.CannonSphereReflection.reflection_image_closedBall line 359
  47. lemma OAI.CannonSphereReflection.onePoint_image line 401
  48. theorem OAI.CannonSphereReflection.exists_convex_reflection line 406