OAI/Geometry/SmoothYau/DifferentialEq/SphericalOpenFormNorm.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.sphericalPositiveSet line 14
  2. abbrev OAI.YauCounterexamples.SphericalPositiveTensor line 16
  3. def OAI.YauCounterexamples.sphericalTensorMetric line 17
  4. lemma OAI.YauCounterexamples.sphericalPositiveSet_isOpen line 21
  5. lemma OAI.YauCounterexamples.sphericalTensorOf_positive line 25
  6. lemma OAI.YauCounterexamples.sphericalTensorMetric_of line 29
  7. lemma OAI.YauCounterexamples.sphericalPositive_zero line 34
  8. lemma OAI.YauCounterexamples.sphericalTensorMetric_zero line 37
  9. lemma OAI.YauCounterexamples.sphericalTensorMetric_family line 40
  10. def OAI.YauCounterexamples.SphericalMetricGood line 49
  11. lemma OAI.YauCounterexamples.sphericalMetricGood_neighborhood line 53
  12. lemma OAI.YauCounterexamples.exists_spherical_open_model line 58