OAI/Geometry/KahlerSplitting/ProductCharts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniversalCoverSplitting.holomorphic_frobenius line 33
  2. lemma OAI.UniversalCoverSplitting.projection_complement_idempotent line 74
  3. lemma OAI.UniversalCoverSplitting.projection_complement_range line 80
  4. lemma OAI.UniversalCoverSplitting.projection_complement_ker line 93
  5. lemma OAI.UniversalCoverSplitting.complement_fixed_iff_zero line 105
  6. theorem OAI.UniversalCoverSplitting.combine_foliation_charts line 120
  7. theorem OAI.UniversalCoverSplitting.holomorphic_product_coordinates line 172
  8. theorem OAI.UniversalCoverSplitting.local_product_chart line 216
  9. structure OAI.UniversalCoverSplitting.SplittingChart line 335
  10. theorem OAI.UniversalCoverSplitting.restrict_product_chart line 347
  11. theorem OAI.UniversalCoverSplitting.exists_splittingChart line 386
  12. lemma OAI.UniversalCoverSplitting.SplittingChart.inverse_derivative line 398
  13. theorem OAI.UniversalCoverSplitting.SplittingChart.box_coordinates line 418
  14. theorem OAI.UniversalCoverSplitting.SplittingChart.box_of_coordinate_tangencies line 439