OAI/Geometry/KahlerSplitting/ShellFilling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalCoverSplitting.IsMixedBox.slice_holomorphic line 33
  2. lemma OAI.UniversalCoverSplitting.IsMixedBox.fibre_eq_of_shell line 41
  3. def OAI.UniversalCoverSplitting.MixedFillable line 57
  4. lemma OAI.UniversalCoverSplitting.mixedFillable_subset line 63
  5. lemma OAI.UniversalCoverSplitting.ball_subset_mixedFillable line 69
  6. lemma OAI.UniversalCoverSplitting.isOpen_mixedFillable line 79
  7. theorem OAI.UniversalCoverSplitting.glue_all_mixed_fillings line 86
  8. lemma OAI.UniversalCoverSplitting.first_affine_slope line 120
  9. theorem OAI.UniversalCoverSplitting.radial_disk_area_bound line 144
  10. theorem OAI.UniversalCoverSplitting.ball_subset_of_closedBall_continuation line 202
  11. lemma OAI.UniversalCoverSplitting.mixedFillable_closedBall line 225
  12. theorem OAI.UniversalCoverSplitting.mixedFillable_uniform_local_continuation line 258
  13. theorem OAI.UniversalCoverSplitting.subset_of_uniform_local_continuation line 291
  14. theorem OAI.UniversalCoverSplitting.mixed_shell_extension line 326
  15. theorem OAI.UniversalCoverSplitting.mixed_hartogs_extension line 347