OAI/Geometry/SmoothYau/Smoothness/ThreeRadiusNormedSpace.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.threeChartMetric line 15
  2. lemma OAI.YauCounterexamples.threeChartMetric_selfFlat line 21
  3. lemma OAI.YauCounterexamples.threeChartMetric_background line 26
  4. lemma OAI.YauCounterexamples.threeChartMetric_background_zero line 32
  5. lemma OAI.YauCounterexamples.threeChartMetric_background_first line 39
  6. lemma OAI.YauCounterexamples.threeChartMetric_background_Christoffel line 48
  7. lemma OAI.YauCounterexamples.threeChartMetric_background_hessian line 55
  8. def OAI.YauCounterexamples.threeSphereMap line 70
  9. lemma OAI.YauCounterexamples.threeSphereMap_smooth line 72
  10. lemma OAI.YauCounterexamples.threeSphereMap_zero line 74
  11. lemma OAI.YauCounterexamples.threeSphereMap_first line 76
  12. lemma OAI.YauCounterexamples.threeSphereMap_second line 82
  13. def OAI.YauCounterexamples.threeSphereCoord line 91
  14. lemma OAI.YauCounterexamples.threeSphereCoord_smooth line 93
  15. lemma OAI.YauCounterexamples.threeSphereCoord_zero line 95
  16. lemma OAI.YauCounterexamples.threeSphereCoord_first line 98
  17. lemma OAI.YauCounterexamples.threeSphereCoord_second line 105
  18. def OAI.YauCounterexamples.threeRadiusSq line 112
  19. lemma OAI.YauCounterexamples.threeRadiusSq_smooth line 114
  20. lemma OAI.YauCounterexamples.threeRadiusSq_zero line 116
  21. lemma OAI.YauCounterexamples.threeRadiusSq_first line 119
  22. lemma OAI.YauCounterexamples.threeRadiusSq_second line 128