OAI/Geometry/SplitTangent/PositiveCoverLift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Positive Cover Lift.

  1. def OAI.SplitTangent.coverTangentLift line 20
  2. lemma OAI.SplitTangent.coverTangentLift_leftInverse line 25
  3. lemma OAI.SplitTangent.coverTangentLift_eq_localInverse line 31
  4. lemma OAI.SplitTangent.coverTangentLift_holomorphic line 55
  5. def OAI.SplitTangent.RationalCurve.coverSection line 79
  6. theorem OAI.SplitTangent.RationalCurve.pointedGenerated_cover_lift line 106
  7. theorem OAI.SplitTangent.RationalCurve.exists_positive_cover_lift line 121
  8. theorem OAI.SplitTangent.RationalCurve.exists_positive_cover_lift_at line 133