OAI/Geometry/SmoothYau/Limits/CoordinateForm.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.CoordinateForm line 16
  2. def OAI.YauCounterexamples.quadraticPlaneStrict line 23
  3. def OAI.YauCounterexamples.quadraticPlaneFull line 26
  4. def OAI.YauCounterexamples.metricProfileTraceForm line 29
  5. lemma OAI.YauCounterexamples.metricProfileTraceForm_apply line 33
  6. lemma OAI.YauCounterexamples.continuous_metricProfileTraceForm line 39
  7. theorem OAI.YauCounterexamples.quadraticPlaneStrict_eventually line 49
  8. theorem OAI.YauCounterexamples.isOpen_quadraticPlaneFull line 82
  9. theorem OAI.YauCounterexamples.compact_quadraticPlaneFull_margin line 108
  10. theorem OAI.YauCounterexamples.compact_variableMetric_margin line 149
  11. lemma OAI.YauCounterexamples.quadraticPlaneFull_pos line 174
  12. def OAI.YauCounterexamples.twoCoframeForm line 192
  13. lemma OAI.YauCounterexamples.twoCoframeForm_apply line 198
  14. lemma OAI.YauCounterexamples.continuous_twoCoframeForm line 204
  15. def OAI.YauCounterexamples.scaledSubForm line 213
  16. lemma OAI.YauCounterexamples.scaledSubForm_apply line 216
  17. lemma OAI.YauCounterexamples.continuousAt_scaledSubForm line 221
  18. theorem OAI.YauCounterexamples.twoCoframe_bounds_eventually line 226