OAI/Geometry/KahlerSplitting/SwapSplitting.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalCoverSplitting.HolomorphicSplitting.complement_range line 13
  2. lemma OAI.UniversalCoverSplitting.HolomorphicSplitting.complement_ker line 26
  3. def OAI.UniversalCoverSplitting.HolomorphicSplitting.swap line 37
  4. lemma OAI.UniversalCoverSplitting.complementaryProjection_swap line 51
  5. def OAI.UniversalCoverSplitting.SplittingChart.swapChart line 59
  6. lemma OAI.UniversalCoverSplitting.SplittingChart.swapChart_holomorphic line 78
  7. lemma OAI.UniversalCoverSplitting.SplittingChart.swapChart_derivative line 85
  8. def OAI.UniversalCoverSplitting.SplittingChart.swap line 98
  9. lemma OAI.UniversalCoverSplitting.HolomorphicSplitting.swap_swap line 134
  10. def OAI.UniversalCoverSplitting.CoverProductChart.swapChart line 141
  11. def OAI.UniversalCoverSplitting.CoverProductChart.swap line 160
  12. lemma OAI.UniversalCoverSplitting.CoverProductChart.swap_derivative line 180
  13. lemma OAI.UniversalCoverSplitting.SplittingChart.cast_chart line 193
  14. lemma OAI.UniversalCoverSplitting.horizontal_swap_of_vertical line 200
  15. lemma OAI.UniversalCoverSplitting.vertical_swap_of_horizontal line 211
  16. lemma OAI.UniversalCoverSplitting.horizontal_of_vertical_swap line 222
  17. lemma OAI.UniversalCoverSplitting.vertical_of_horizontal_swap line 228