OAI/Geometry/KahlerSplitting/ContinuousBoxes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProductBoxTopology.IsBox line 15
2. lemma OAI.ProductBoxTopology.IsBox.separated line 20
3. theorem OAI.ProductBoxTopology.unique line 37
4. lemma OAI.ProductBoxTopology.locallyConstant_of_finite_closed_cover line 118
5. lemma OAI.ProductBoxTopology.locallyConstant_source_of_finite_closed_cover line 135
6. lemma OAI.ProductBoxTopology.IsBox.precomp line 149
7. lemma OAI.ProductBoxTopology.IsBox.of_closed_rectangles line 164
8. lemma OAI.UniversalCoverSplitting.locallyConstant_restrict_of_fderiv_zero line 199
9. def OAI.UniversalCoverSplitting.splittingAtlas line 209
10. lemma OAI.UniversalCoverSplitting.IsBlockBox.plaqueBox line 213
11. lemma OAI.ProductBoxTopology.unique_paths line 279
12. lemma OAI.ProductBoxTopology.unique_connected line 291
13. lemma OAI.ProductBoxTopology.pathConnected_Icc_unit line 301