OAI/Geometry/KahlerSplitting/RetractCharts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniversalCoverSplitting.RetractChart line 13
2. lemma OAI.UniversalCoverSplitting.restrict_retract_chart line 23
3. abbrev OAI.UniversalCoverSplitting.RetractChart.Fixed line 61
4. lemma OAI.UniversalCoverSplitting.RetractChart.fixed_iff line 63
5. lemma OAI.UniversalCoverSplitting.RetractChart.fixed_inverse line 73
6. def OAI.UniversalCoverSplitting.RetractChart.fixedInv line 80
7. lemma OAI.UniversalCoverSplitting.RetractChart.fixedInv_val line 85
8. lemma OAI.UniversalCoverSplitting.RetractChart.continuousOn_fixedInv line 88
9. def OAI.UniversalCoverSplitting.RetractChart.fixedChart line 94
10. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.exists_retractChart line 134
11. structure OAI.UniversalCoverSplitting.CoverProductChart line 172
12. lemma OAI.UniversalCoverSplitting.exists_coverProductChart line 183
13. lemma OAI.UniversalCoverSplitting.CoverProductChart.down_inverse line 216
14. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.plaque_constant line 239
15. lemma OAI.UniversalCoverSplitting.FirstGerm.GlobalProjection.chart_factor line 274