OAI/Geometry/KahlerSplitting/BoundaryExtension.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalCoverSplitting.exists_boundary_scales line 34
  2. theorem OAI.UniversalCoverSplitting.exists_boundary_chart_annulus line 76
  3. lemma OAI.UniversalCoverSplitting.IsMixedBox.eqOn_of_slice_in_domain line 138
  4. theorem OAI.UniversalCoverSplitting.mixed_boundary_extension_of_shrinking_slices line 172
  5. def OAI.UniversalCoverSplitting.separatedHomeomorph line 233
  6. lemma OAI.UniversalCoverSplitting.separatedHomeomorph_apply line 244
  7. lemma OAI.UniversalCoverSplitting.separatedHomeomorph_symm_apply line 247
  8. lemma OAI.UniversalCoverSplitting.separatedAffine_convex_preimage line 251
  9. lemma OAI.UniversalCoverSplitting.IsBox.comp_separatedHomeomorph_symm line 257
  10. lemma OAI.UniversalCoverSplitting.contDiffAt_quadratic_remainder line 270
  11. lemma OAI.UniversalCoverSplitting.exists_parabolic_interior_disks line 303
  12. def OAI.UniversalCoverSplitting.mixedSource line 363
  13. lemma OAI.UniversalCoverSplitting.mixedSource_zero line 367
  14. theorem OAI.UniversalCoverSplitting.affine_mixed_boundary_extension line 373