OAI/Geometry/Cannon/Conformal/RestrictedSphereAction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CannonMobius.restrictedSphereAction line 19
2. lemma OAI.CannonMobius.sphereDerivative_one line 29
3. lemma OAI.CannonMobius.continuous_derivativeMatrix line 38
4. lemma OAI.CannonMobius.measurable_sphereDerivative_on line 42
5. lemma OAI.CannonMobius.continuous_normalized_round line 51
6. lemma OAI.CannonMobius.measurable_normalized_round line 63
7. lemma OAI.CannonMobius.measurable_normalized_round_on line 74
8. theorem OAI.CannonMobius.controlled_action_invariant_structure line 80