OAI/Geometry/SmoothYau/SphereMetric/FourThree.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.ThreeManifold line 15
  2. abbrev OAI.YauCounterexamples.ThreeProductModel line 16
  3. abbrev OAI.YauCounterexamples.ThreeModel line 17
  4. abbrev OAI.YauCounterexamples.ThreeAmbient line 18
  5. instance OAI.YauCounterexamples.threeProductChartedSpace line 19
  6. instance OAI.YauCounterexamples.threeProductIsManifold line 21
  7. abbrev OAI.YauCounterexamples.threeModelEquiv line 24
  8. instance OAI.YauCounterexamples.threeChartedSpace line 26
  9. instance OAI.YauCounterexamples.threeIsManifold line 28
  10. def OAI.YauCounterexamples.threeImmersion line 31
  11. lemma OAI.YauCounterexamples.threeImmersion_product_smooth line 33
  12. lemma OAI.YauCounterexamples.threeImmersion_smooth line 37
  13. lemma OAI.YauCounterexamples.threeImmersion_injective line 39
  14. def OAI.YauCounterexamples.threeBackgroundMetric line 49
  15. lemma OAI.YauCounterexamples.threeModel_finrank line 52
  16. instance OAI.YauCounterexamples.circle_dimension_fact line 64
  17. def OAI.YauCounterexamples.threeFrame line 65
  18. def OAI.YauCounterexamples.threeChartMap line 67
  19. lemma OAI.YauCounterexamples.three_chart_symm line 70
  20. lemma OAI.YauCounterexamples.three_chart_center line 79
  21. lemma OAI.YauCounterexamples.three_chart_target line 84
  22. lemma OAI.YauCounterexamples.three_coordinate_embedding line 95
  23. lemma OAI.YauCounterexamples.three_metricCoefficients line 107
  24. lemma OAI.YauCounterexamples.three_metricCoefficients_zero line 113
  25. lemma OAI.YauCounterexamples.three_metricCoefficients_first line 121
  26. lemma OAI.YauCounterexamples.three_metricFirstCoefficient_zero line 127
  27. theorem OAI.YauCounterexamples.three_laplace_at_center line 134
  28. lemma OAI.YauCounterexamples.three_simple_eigenpair_open line 151
  29. def OAI.YauCounterexamples.fourToThree line 203
  30. def OAI.YauCounterexamples.fourToCircle line 204
  31. lemma OAI.YauCounterexamples.fourToThree_product_smooth line 205
  32. lemma OAI.YauCounterexamples.fourToThree_smooth line 209
  33. lemma OAI.YauCounterexamples.fourToCircle_smooth line 211
  34. lemma OAI.YauCounterexamples.mfderiv_fourToThree line 215
  35. lemma OAI.YauCounterexamples.mfderiv_fourToCircle line 227
  36. def OAI.YauCounterexamples.circleRoundMetric line 235