OAI/Geometry/SmoothYau/ProductMetric/ThreeMeridianNormedSpace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.threeMeridianAmbient line 14
  2. lemma OAI.YauCounterexamples.threeMeridianAmbient_norm line 15
  3. def OAI.YauCounterexamples.threeMeridian line 22
  4. lemma OAI.YauCounterexamples.threeMeridian_smooth line 24
  5. lemma OAI.YauCounterexamples.threeMeridian_A line 31
  6. lemma OAI.YauCounterexamples.threeMeridian_B line 33
  7. lemma OAI.YauCounterexamples.threeMeridian_circle line 35
  8. lemma OAI.YauCounterexamples.complex_I_pow_four_add_one line 36
  9. lemma OAI.YauCounterexamples.complex_I_pow_four line 39
  10. lemma OAI.YauCounterexamples.complex_neg_one_pow_four_add_one line 40
  11. lemma OAI.YauCounterexamples.threeMeridian_complex line 43
  12. lemma OAI.YauCounterexamples.threeMeridian_zero line 50
  13. lemma OAI.YauCounterexamples.threeMeridian_gradient_value line 53