OAI/Geometry/KahlerSplitting/PlaqueCharts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ProductBoxTopology.ProductChart line 13
2. lemma OAI.ProductBoxTopology.ProductChart.parameter_tile line 21
3. lemma OAI.UniversalCoverSplitting.IsBox.isBlockBox line 98
4. def OAI.UniversalCoverSplitting.SplittingChart.productChart line 119
5. lemma OAI.UniversalCoverSplitting.splittingProductCharts_cover line 131
6. lemma OAI.UniversalCoverSplitting.IsBlockBox.of_local line 141
7. lemma OAI.UniversalCoverSplitting.IsBlockBox.congr line 152
8. abbrev OAI.UniversalCoverSplitting.unitComplex line 177
9. lemma OAI.UniversalCoverSplitting.norm_unitComplex line 179
10. lemma OAI.UniversalCoverSplitting.continuous_unitComplex line 182
11. lemma OAI.UniversalCoverSplitting.smul_unit_ball line 185
12. lemma OAI.UniversalCoverSplitting.radial_scaled_ball line 190
13. theorem OAI.UniversalCoverSplitting.exists_radial_plaque_box line 200
14. theorem OAI.UniversalCoverSplitting.block_endpoint_of_family line 249