OAI/Geometry/Cannon/Conformal/MarkedChart.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CannonMobius.markedChart line 15
2. lemma OAI.CannonMobius.markedChart_biholomorphic line 16
3. lemma OAI.CannonMobius.markedChart_isometry line 23
4. lemma OAI.CannonMobius.markedChart_pole line 28
5. lemma OAI.CannonMobius.markedChart_other line 36
6. lemma OAI.CannonMobius.coordinate_bound_away_pole line 52
7. lemma OAI.CannonMobius.coordinate_comparison line 65