OAI/Geometry/KahlerSplitting/FixedManifolds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniversalCoverSplitting.RetractChart.differentiableOn_transition line 14
2. lemma OAI.UniversalCoverSplitting.RetractChart.contDiffOn_transition line 35
3. def OAI.UniversalCoverSplitting.RetractChart.fixedChartedSpace line 44
4. lemma OAI.UniversalCoverSplitting.RetractChart.fixedIsManifold line 50
5. def OAI.UniversalCoverSplitting.RetractChart.fixedManifold line 61
6. lemma OAI.UniversalCoverSplitting.RetractChart.fixed_inclusion_holomorphic line 84
7. lemma OAI.UniversalCoverSplitting.RetractChart.fixed_projection_holomorphic line 105
8. lemma OAI.UniversalCoverSplitting.CoverProductChart.surjective_derivative line 134
9. lemma OAI.UniversalCoverSplitting.CoverProductChart.surjective_first_derivative line 150
10. lemma OAI.UniversalCoverSplitting.CoverProductChart.surjective_factor_iff line 167
11. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.vertical_reach line 216
12. lemma OAI.UniversalCoverSplitting.surjective_mfderiv_of_rightInverse line 267
13. lemma OAI.UniversalCoverSplitting.surjective_along_vertical line 280
14. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.submersion line 310