OAI/Geometry/SplitTangent/HolomorphicManifoldProduct.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Holomorphic Manifold Product.

  1. lemma OAI.SplitTangent.TangentSplitting.coordinateProjector_range line 18
  2. lemma OAI.SplitTangent.TangentSplitting.coordinateProjector_kernel line 33
  3. abbrev OAI.SplitTangent.TangentSplitting.FirstModel line 42
  4. abbrev OAI.SplitTangent.TangentSplitting.SecondModel line 44
  5. theorem OAI.SplitTangent.TangentSplitting.exists_local_product_chart line 49
  6. theorem OAI.SplitTangent.TangentSplitting.exists_aligned_product_chart line 119
  7. theorem OAI.SplitTangent.TangentSplitting.exists_aligned_product_chartAlternative line 146