OAI/Geometry/Kahler/Obstruction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs.ball_eq line 12
  2. lemma OAI.PinchedHartogs.isOpen_ball line 16
  3. lemma OAI.PinchedHartogs.zero_mem_ball line 20
  4. lemma OAI.PinchedHartogs.simplyConnected_ball line 22
  5. lemma OAI.PinchedHartogs.zeroSection_mem line 29
  6. lemma OAI.PinchedHartogs.analyticAt_of_exp_eq line 32
  7. lemma OAI.PinchedHartogs.exists_holomorphic_log line 50
  8. lemma OAI.PinchedHartogs.norm_deriv_le_on_open_disk line 64
  9. lemma OAI.PinchedHartogs.cauchy_direction line 78
  10. lemma OAI.PinchedHartogs.analytic_jacobian_zero line 100
  11. lemma OAI.PinchedHartogs.base_line_mem line 122
  12. lemma OAI.PinchedHartogs.jacobian_base_bound line 136
  13. lemma OAI.PinchedHartogs.exp_fiber_identity line 149
  14. lemma OAI.PinchedHartogs.fiber_line_mem line 153
  15. lemma OAI.PinchedHartogs.jacobian_fiber_bound line 165
  16. lemma OAI.PinchedHartogs.det_bound_columns line 173
  17. lemma OAI.PinchedHartogs.jacobian_det_bound line 213
  18. lemma OAI.PinchedHartogs.jacobian_log_bound line 228
  19. theorem OAI.PinchedHartogs.map_obstruction line 249