OAI/Geometry/Cannon/Conformal/SphereTile.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonEmbeddedArc.Arc.sphereTile line 22
  2. lemma OAI.CannonEmbeddedArc.Arc.sphereTile_closed line 26
  3. lemma OAI.CannonEmbeddedArc.Arc.sphereTile_cover line 34
  4. theorem OAI.CannonEmbeddedArc.Arc.sphereTile_inter_common_vertex line 48
  5. lemma OAI.CannonEmbeddedArc.Arc.compactifiedFace_vertex line 101
  6. lemma OAI.CannonEmbeddedArc.Arc.compactifiedFace_preconnected line 106
  7. theorem OAI.CannonEmbeddedArc.Arc.sphere_carrier_preconnected line 111
  8. theorem OAI.CannonEmbeddedArc.Arc.sphere_realization_fiber_bound line 132
  9. lemma OAI.CannonMobius.inv_inv_apply line 164
  10. lemma OAI.CannonMobius.inv_scalar_differentiable line 166
  11. lemma OAI.CannonMobius.isAnalytic_one line 172
  12. lemma OAI.CannonMobius.isAnalytic_inversion line 183
  13. def OAI.CannonMobius.affinePlane line 197
  14. def OAI.CannonMobius.affine line 205
  15. lemma OAI.CannonMobius.affine_infty line 206
  16. lemma OAI.CannonMobius.affine_coe line 207
  17. lemma OAI.CannonMobius.affine_symm line 210
  18. lemma OAI.CannonMobius.inChart_affine_tt line 221
  19. lemma OAI.CannonMobius.isAnalytic_affine line 232
  20. def OAI.CannonMobius.biholomorphic line 276
  21. lemma OAI.CannonMobius.affine_biholomorphic line 284
  22. lemma OAI.CannonMobius.inversion_biholomorphic line 289
  23. def OAI.CannonMobius.std line 297
  24. lemma OAI.CannonMobius.std_injective line 298
  25. abbrev OAI.CannonMobius.Triple line 302
  26. def OAI.CannonMobius.standard line 303
  27. def OAI.CannonMobius.tripleMap line 304
  28. lemma OAI.CannonMobius.continuous_tripleMap line 305
  29. def OAI.CannonMobius.tripleHomeomorph line 310
  30. lemma OAI.CannonMobius.tripleMap_mul line 317
  31. lemma OAI.CannonMobius.exists_finite_normalizer line 320
  32. lemma OAI.CannonMobius.exists_pole_avoiding line 357
  33. lemma OAI.CannonMobius.exists_triple_normalizer line 366
  34. lemma OAI.CannonMobius.sphere_locallyPathConnected line 395
  35. theorem OAI.CannonMobius.normalize_finite_realization line 408
  36. theorem OAI.CannonMobius.normalized_carrier line 430