OAI/Geometry/SmoothYau/Limits/PlanePairMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.planePairMap line 21
  2. def OAI.YauCounterexamples.tangentProjection line 26
  3. lemma OAI.YauCounterexamples.tangentProjection_apply line 29
  4. lemma OAI.YauCounterexamples.planePairMap_apply line 32
  5. def OAI.YauCounterexamples.projectedPlaneMap line 35
  6. lemma OAI.YauCounterexamples.projectedPlaneMap_tangent line 38
  7. lemma OAI.YauCounterexamples.projectedPlaneMap_norm_sq line 43
  8. lemma OAI.YauCounterexamples.projectedPlaneMap_quadratic line 56
  9. lemma OAI.YauCounterexamples.plane_cauchy line 78
  10. lemma OAI.YauCounterexamples.projectedPlaneMap_lower line 82
  11. lemma OAI.YauCounterexamples.projectedPlaneMap_injective line 90
  12. lemma OAI.YauCounterexamples.projectedPlaneMap_quadratic_lower line 106