OAI/Geometry/KahlerSplitting/MixedShell.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalCoverSplitting.complexAnnulus line 32
  2. lemma OAI.UniversalCoverSplitting.isOpen_complexAnnulus line 34
  3. lemma OAI.UniversalCoverSplitting.complexAnnulus_subset_ball line 37
  4. lemma OAI.UniversalCoverSplitting.complexAnnulus_nonempty line 40
  5. lemma OAI.UniversalCoverSplitting.isPreconnected_complexAnnulus line 46
  6. lemma OAI.UniversalCoverSplitting.complexAnnulus_inter_ball line 63
  7. lemma OAI.UniversalCoverSplitting.complexAnnulus_union_ball line 69
  8. lemma OAI.UniversalCoverSplitting.box_shifted_diagonal_germ_unique line 89
  9. lemma OAI.UniversalCoverSplitting.IsMixedBox.eqOn_of_slice line 123
  10. theorem OAI.UniversalCoverSplitting.holomorphic_curve_mixed_thickening line 158
  11. lemma OAI.UniversalCoverSplitting.glue_mixed_boxes line 188
  12. lemma OAI.UniversalCoverSplitting.glue_mixed_boxes_pair line 213
  13. theorem OAI.UniversalCoverSplitting.mixed_shell_fill_of_slice line 240
  14. theorem OAI.UniversalCoverSplitting.mixed_shell_fill_of_bounded_slices line 287
  15. lemma OAI.UniversalCoverSplitting.IsBox.mixed_slope_bound line 334
  16. theorem OAI.UniversalCoverSplitting.exists_uniform_mixed_slope line 356