OAI/Geometry/SplitTangent/BoxFirstTransport.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Box First Transport.

  1. def OAI.SplitTangent.TangentSplitting.canonicalChartImages line 21
  2. def OAI.SplitTangent.TangentSplitting.entireMap line 25
  3. lemma OAI.SplitTangent.TangentSplitting.entireMap_congr line 32
  4. lemma OAI.SplitTangent.TangentSplitting.entireMap_self line 43
  5. lemma OAI.SplitTangent.TangentSplitting.entireMap_family_holomorphic_at line 50
  6. lemma OAI.SplitTangent.TangentBox.vertical_holomorphic line 73
  7. lemma OAI.SplitTangent.TangentBox.vertical_tangent line 77
  8. def OAI.SplitTangent.TangentBox.vertical line 91
  9. def OAI.SplitTangent.TangentBox.chartTransport line 100
  10. lemma OAI.SplitTangent.TangentBox.chartTransport_self line 104
  11. lemma OAI.SplitTangent.TangentBox.chartTransport_horizontal_overlap line 108
  12. lemma OAI.SplitTangent.TangentBox.chartTransport_vertical_overlap line 115
  13. lemma OAI.SplitTangent.TangentBox.chartTransport_holomorphic_at line 124
  14. lemma OAI.SplitTangent.TangentBox.vertical_one line 135
  15. lemma OAI.SplitTangent.TangentBox.section_holomorphic_congr_base line 139
  16. def OAI.SplitTangent.TangentBox.firstMap line 151
  17. lemma OAI.SplitTangent.TangentBox.firstMap_normalized line 178
  18. theorem OAI.SplitTangent.TangentBox.exists_normalized_factor_transport line 184