OAI/Geometry/SmoothYau/Smoothness/ProductSphereFstPower.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.productSphere_fstPower line 18
  2. lemma OAI.YauCounterexamples.productSphere_fstPower_smooth line 23
  3. lemma OAI.YauCounterexamples.productSphere_fstPower_zero line 28
  4. lemma OAI.YauCounterexamples.productSphere_fstPower_first line 32
  5. lemma OAI.YauCounterexamples.productSphere_fstPower_second line 43
  6. lemma OAI.YauCounterexamples.productSphere_fstPower_trace line 55
  7. def OAI.YauCounterexamples.productSphere_sndPower line 91
  8. lemma OAI.YauCounterexamples.productSphere_sndPower_smooth line 96
  9. lemma OAI.YauCounterexamples.productSphere_sndPower_zero line 101
  10. lemma OAI.YauCounterexamples.productSphere_sndPower_first line 105
  11. lemma OAI.YauCounterexamples.productSphere_sndPower_second line 116
  12. lemma OAI.YauCounterexamples.productSphere_sndPower_trace line 128