OAI/Analysis/DirectCrouzeix/InverseExterior.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.Geometry.inverseExterior line 41
  2. theorem OAI.DirectCrouzeix.Geometry.zero_mem_inverseExterior line 43
  3. theorem OAI.DirectCrouzeix.Geometry.mem_inverseExterior_iff line 45
  4. theorem OAI.DirectCrouzeix.Geometry.inverseExterior_isOpen line 48
  5. theorem OAI.DirectCrouzeix.Geometry.inverseExterior_starConvex line 78
  6. theorem OAI.DirectCrouzeix.Geometry.inverseExterior_simplyConnected line 105
  7. theorem OAI.DirectCrouzeix.Geometry.inverseExterior_bounded line 112
  8. theorem OAI.DirectCrouzeix.Geometry.inverseExterior_compact_closure line 129
  9. theorem OAI.DirectCrouzeix.Geometry.inverseExterior_proper line 135
  10. theorem OAI.DirectCrouzeix.Geometry.inverseExterior_frontier_level line 143