OAI/Geometry/SmoothYau/Smoothness/TorusAmbient.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.productImmersion line 18
  2. lemma OAI.YauCounterexamples.productImmersion_smooth line 22
  3. lemma OAI.YauCounterexamples.productImmersion_derivative line 33
  4. lemma OAI.YauCounterexamples.productImmersion_injective_derivative line 56
  5. abbrev OAI.YauCounterexamples.TorusAmbient line 72
  6. abbrev OAI.YauCounterexamples.FourAmbient line 73
  7. def OAI.YauCounterexamples.torusImmersion line 75
  8. lemma OAI.YauCounterexamples.circle_immersion_smooth line 78
  9. lemma OAI.YauCounterexamples.circle_immersion_injective line 83
  10. lemma OAI.YauCounterexamples.torusImmersion_smooth line 88
  11. lemma OAI.YauCounterexamples.torusImmersion_injective line 93
  12. def OAI.YauCounterexamples.fourImmersion line 100
  13. lemma OAI.YauCounterexamples.sphere_two_immersion_smooth line 103
  14. lemma OAI.YauCounterexamples.sphere_two_immersion_injective line 108
  15. lemma OAI.YauCounterexamples.fourImmersion_smooth line 114
  16. lemma OAI.YauCounterexamples.fourImmersion_injective line 119
  17. def OAI.YauCounterexamples.fourBackgroundMetric line 126
  18. lemma OAI.YauCounterexamples.fourBackgroundMetric_inner line 129