OAI/Geometry/KahlerSplitting/ProductRetracts.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalCoverSplitting.simplyConnected_fixed line 11
  2. lemma OAI.UniversalCoverSplitting.integrable_swap_complement line 56
  3. structure OAI.UniversalCoverSplitting.ProductRetracts line 59
  4. lemma OAI.UniversalCoverSplitting.exists_productRetracts line 68
  5. def OAI.UniversalCoverSplitting.ProductRetracts.Y₁ line 84
  6. def OAI.UniversalCoverSplitting.ProductRetracts.Y₂ line 85
  7. def OAI.UniversalCoverSplitting.ProductRetracts.q₁ line 89
  8. def OAI.UniversalCoverSplitting.ProductRetracts.q₂ line 90
  9. def OAI.UniversalCoverSplitting.ProductRetracts.pair line 91
  10. lemma OAI.UniversalCoverSplitting.ProductRetracts.q₁_holomorphic line 93
  11. lemma OAI.UniversalCoverSplitting.ProductRetracts.q₂_holomorphic line 96
  12. lemma OAI.UniversalCoverSplitting.ProductRetracts.pair_holomorphic line 99
  13. lemma OAI.UniversalCoverSplitting.ProductRetracts.q₁_submersion line 102
  14. lemma OAI.UniversalCoverSplitting.ProductRetracts.q₂_submersion line 104
  15. lemma OAI.UniversalCoverSplitting.ProductRetracts.q₁_factor line 107
  16. lemma OAI.UniversalCoverSplitting.ProductRetracts.q₂_factor line 111
  17. lemma OAI.UniversalCoverSplitting.ProductRetracts.simplyConnected_first line 117
  18. lemma OAI.UniversalCoverSplitting.ProductRetracts.simplyConnected_second line 121
  19. lemma OAI.UniversalCoverSplitting.CoverProductChart.factor_kernel line 139