OAI/Geometry/KahlerSplitting/PathBoxes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProductBoxTopology.IsHorizontal line 13
2. def OAI.ProductBoxTopology.IsVertical line 17
3. lemma OAI.ProductBoxTopology.IsBox.horizontal line 21
4. lemma OAI.ProductBoxTopology.IsBox.vertical line 26
5. lemma OAI.ProductBoxTopology.IsHorizontal.precomp line 31
6. lemma OAI.ProductBoxTopology.IsVertical.precomp line 38
7. lemma OAI.UniversalCoverSplitting.horizontal_local_parameter line 53
8. lemma OAI.UniversalCoverSplitting.vertical_local_parameter line 87
9. theorem OAI.ClosedCoverGlue.exists_glue line 133
10. theorem OAI.ProductBoxTopology.grid_glue line 161
11. theorem OAI.UniversalCoverSplitting.path_axes line 221
12. lemma OAI.UniversalCoverSplitting.continuous_local_parameter line 285
13. theorem OAI.UniversalCoverSplitting.path_diagonal line 306