OAI/Geometry/KahlerSplitting/GermTransport.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniversalCoverSplitting.SplittingChart.firstProjection line 13
2. lemma OAI.UniversalCoverSplitting.SplittingChart.firstProjection_target line 16
3. lemma OAI.UniversalCoverSplitting.SplittingChart.firstProjection_source line 23
4. lemma OAI.UniversalCoverSplitting.SplittingChart.firstProjection_coordinates line 27
5. lemma OAI.UniversalCoverSplitting.SplittingChart.firstProjection_holomorphic line 32
6. lemma OAI.UniversalCoverSplitting.SplittingChart.firstProjection_self line 42
7. lemma OAI.UniversalCoverSplitting.FirstGerm.extends_plaque line 48
8. theorem OAI.IntervalChain.lift_cells line 106
9. lemma OAI.UniversalCoverSplitting.FirstGerm.lift_chart line 160
10. lemma OAI.UniversalCoverSplitting.FirstGerm.lift_vertical line 184
11. lemma OAI.UniversalCoverSplitting.independent_first_of_fderiv_zero line 222
12. lemma OAI.UniversalCoverSplitting.SplittingChart.transition_second line 245
13. lemma OAI.UniversalCoverSplitting.SplittingChart.firstProjection_germ_eq line 279
14. def OAI.UniversalCoverSplitting.FirstGerm.projection line 312
15. lemma OAI.UniversalCoverSplitting.FirstGerm.projection_first line 321
16. lemma OAI.UniversalCoverSplitting.FirstGerm.projection_eq line 325