OAI/Geometry/KahlerSplitting/BlockMaps.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniversalCoverSplitting.IsBlockBox line 15
2. lemma OAI.UniversalCoverSplitting.IsBlockBox.mono line 21
3. lemma OAI.UniversalCoverSplitting.SplittingChart.block_coordinates line 25
4. lemma OAI.UniversalCoverSplitting.SplittingChart.block_of_coordinate_tangencies line 44
5. lemma OAI.UniversalCoverSplitting.SplittingChart.inverse_isBlockBox line 68
6. lemma OAI.UniversalCoverSplitting.SplittingChart.mix_block_maps line 74
7. def OAI.UniversalCoverSplitting.IsHorizontalMap line 110
8. def OAI.UniversalCoverSplitting.IsVerticalMap line 114
9. lemma OAI.UniversalCoverSplitting.IsHorizontalMap.comp line 118
10. lemma OAI.UniversalCoverSplitting.IsVerticalMap.comp line 127
11. lemma OAI.UniversalCoverSplitting.IsHorizontalMap.curve line 136
12. lemma OAI.UniversalCoverSplitting.IsVerticalMap.curve line 139
13. lemma OAI.UniversalCoverSplitting.IsHorizontalMap.block line 142
14. lemma OAI.UniversalCoverSplitting.IsVerticalMap.block line 159
15. lemma OAI.UniversalCoverSplitting.IsBlockBox.comp_parameters line 193
16. lemma OAI.UniversalCoverSplitting.IsBlockBox.horizontal_slice line 242
17. lemma OAI.UniversalCoverSplitting.IsBlockBox.vertical_slice line 265
18. abbrev OAI.UniversalCoverSplitting.Polydisk line 299
19. def OAI.UniversalCoverSplitting.SplittingChart.unitMap line 301
20. lemma OAI.UniversalCoverSplitting.scale_mem_ball line 304
21. lemma OAI.UniversalCoverSplitting.unscale_mem_ball line 310
22. lemma OAI.UniversalCoverSplitting.SplittingChart.unitMap_block line 316
23. lemma OAI.UniversalCoverSplitting.SplittingChart.unitMap_coordinates line 325