OAI/Geometry/SmoothYau/Smoothness/RoundPowerRadius.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.powerRadiusMap line 14
2. lemma OAI.YauCounterexamples.powerRadiusMap_contDiff line 15
3. lemma OAI.YauCounterexamples.powerRadiusMap_directional line 23
4. theorem OAI.YauCounterexamples.powerRadiusMap_surjective line 52
5. def OAI.YauCounterexamples.roundPowerRadius line 93
6. lemma OAI.YauCounterexamples.roundPowerRadius_chart line 95
7. lemma OAI.YauCounterexamples.roundPowerRadius_chart_contDiff line 101
8. theorem OAI.YauCounterexamples.roundPowerRadius_chart_surjective line 106