OAI/Geometry/SmoothYau/Smoothness/SmDualNorm.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.MetricJet line 45
  2. def OAI.YauCounterexamples.metricJetMap line 48
  3. lemma OAI.YauCounterexamples.contDiff_selfMetricFlat_inverse line 52
  4. lemma OAI.YauCounterexamples.continuous_metricJetMap line 59
  5. def OAI.YauCounterexamples.metricJetStrict line 67
  6. def OAI.YauCounterexamples.metricJetFull line 70
  7. lemma OAI.YauCounterexamples.isOpen_metricJetStrict line 73
  8. lemma OAI.YauCounterexamples.isOpen_metricJetFull line 81
  9. theorem OAI.YauCounterexamples.compact_metricJet_stability line 87
  10. lemma OAI.YauCounterexamples.metricJetStrict_actual line 113
  11. lemma OAI.YauCounterexamples.metricJetFull_actual line 126
  12. def OAI.YauCounterexamples.fullStrictJetMap line 155
  13. def OAI.YauCounterexamples.fullStrictJetSet line 158
  14. lemma OAI.YauCounterexamples.fullStrictJetMap_actual line 161
  15. lemma OAI.YauCounterexamples.continuousAt_fullStrictJetMap line 166
  16. lemma OAI.YauCounterexamples.metricScalarJet_strict_interior line 183
  17. theorem OAI.YauCounterexamples.compact_actual_strict_metric_stability line 195