OAI/Geometry/Kahler/HartogsTopologySupport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs.scaled_fibre_lt line 21
  2. lemma OAI.PinchedHartogs.unscaled_fibre_lt line 27
  3. def OAI.PinchedHartogs.hartogsHomeomorph line 36
  4. theorem OAI.PinchedHartogs.hartogs_contractible line 64
  5. theorem OAI.PinchedHartogs.hartogs_isOpen line 73
  6. theorem OAI.PinchedHartogs.hartogs_nonempty line 86
  7. lemma OAI.PinchedHartogs.coordinate_symm_single line 92
  8. theorem OAI.PinchedHartogs.jacobian_det_ne_of_injective line 99
  9. theorem OAI.PinchedHartogs.no_bounded_realization line 111
  10. theorem OAI.PinchedHartogs.hartogs_obstruction line 148