OAI/Geometry/KahlerSplitting/GlobalProjections.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniversalCoverSplitting.FirstGerm.global_germ line 15
2. lemma OAI.UniversalCoverSplitting.FirstGerm.global_projection line 54
3. lemma OAI.UniversalCoverSplitting.holomorphic_eq_of_eventuallyEq line 93
4. lemma OAI.UniversalCoverSplitting.LocalBiholomorphism.eq_germ_of_comp_eq line 99
5. structure OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection line 123
6. lemma OAI.UniversalCoverSplitting.FirstGerm.exists_globalProjection line 134
7. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.initial_germ line 152
8. lemma OAI.UniversalCoverSplitting.FirstGerm.value_vertical line 163
9. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.horizontal_germs line 185
10. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.horizontal_fixed line 198
11. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.vertical_constant line 217