OAI/Geometry/KahlerSplitting/AxisContinuation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniversalCoverSplitting.box_axes_germ_unique line 35
2. lemma OAI.UniversalCoverSplitting.horizontal_axis_boundary_extension line 82
3. lemma OAI.UniversalCoverSplitting.vertical_axis_boundary_extension line 132
4. lemma OAI.UniversalCoverSplitting.superPotential_norm_bound line 187
5. lemma OAI.UniversalCoverSplitting.superSublevel_compact line 201
6. lemma OAI.UniversalCoverSplitting.superPotential_radial_lt line 210
7. lemma OAI.UniversalCoverSplitting.superDomain_closure line 218
8. lemma OAI.UniversalCoverSplitting.superDomain_frontier line 234
9. lemma OAI.UniversalCoverSplitting.superDomain_axis_closure line 242
10. lemma OAI.UniversalCoverSplitting.superDomain_vertical_axis_closure line 255
11. lemma OAI.UniversalCoverSplitting.superSublevel_subset_bidisk line 268
12. lemma OAI.UniversalCoverSplitting.superSublevel_widen line 273
13. lemma OAI.UniversalCoverSplitting.segment_meets_inter_balls line 300
14. lemma OAI.UniversalCoverSplitting.convex_boundary_ball_overlap line 323
15. lemma OAI.UniversalCoverSplitting.box_extend_closure line 340