OAI/Analysis/Crouzeix/ExteriorRiemann.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exterior Riemann.

  1. def OAI.CrouzeixHilbert.Conformal.invertedExterior line 14
  2. theorem OAI.CrouzeixHilbert.Conformal.zero_mem_invertedExterior line 17
  3. theorem OAI.CrouzeixHilbert.Conformal.invertedExterior_mem_nhds_zero line 20
  4. theorem OAI.CrouzeixHilbert.Conformal.isOpen_invertedExterior line 37
  5. theorem OAI.CrouzeixHilbert.Conformal.isBounded_invertedExterior line 50
  6. theorem OAI.CrouzeixHilbert.Conformal.starConvex_invertedExterior line 67
  7. theorem OAI.CrouzeixHilbert.Conformal.isSimplyConnected_invertedExterior line 85
  8. theorem OAI.CrouzeixHilbert.Conformal.riemann_invertedExterior line 92
  9. theorem OAI.CrouzeixHilbert.Conformal.riemann_exterior line 111