OAI/Geometry/SplitTangent/EmbeddedTangentLift.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Embedded Tangent Lift.

  1. def OAI.SplitTangent.EmbeddedHolomorphicAtlas.retract line 19
  2. lemma OAI.SplitTangent.EmbeddedHolomorphicAtlas.retract_eq line 21
  3. lemma OAI.SplitTangent.EmbeddedHolomorphicAtlas.retract_holomorphic line 26
  4. lemma OAI.SplitTangent.EmbeddedHolomorphicAtlas.retract_comp_inclusion line 38
  5. lemma OAI.SplitTangent.EmbeddedHolomorphicAtlas.retract_mfderiv_leftInverse line 43
  6. def OAI.SplitTangent.EmbeddedHolomorphicAtlas.tangentLift line 56
  7. lemma OAI.SplitTangent.EmbeddedHolomorphicAtlas.tangentLift_leftInverse line 59
  8. lemma OAI.SplitTangent.EmbeddedHolomorphicAtlas.tangentLift_eq_retract line 75
  9. lemma OAI.SplitTangent.EmbeddedHolomorphicAtlas.tangentLift_holomorphic line 86