OAI/Analysis/NumericalRange/ConvexExterior.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompleteCrouzeix.regular_real_normal_coordinates line 43
2. lemma OAI.CompleteCrouzeix.convexBarrier_local_analytic_chart line 83
3. lemma OAI.CompleteCrouzeix.convexBarrier_local_analytic_closed_chart line 144
4. lemma OAI.CompleteCrouzeix.convexBarrier_analytic_chart line 208
5. def OAI.CompleteCrouzeix.invertedExterior line 225
6. lemma OAI.CompleteCrouzeix.zero_mem_invertedExterior line 228
7. lemma OAI.CompleteCrouzeix.invertedExterior_open line 231
8. lemma OAI.CompleteCrouzeix.invertedExterior_bounded line 261
9. lemma OAI.CompleteCrouzeix.invertedExterior_starConvex line 278
10. lemma OAI.CompleteCrouzeix.invertedExterior_simplyConnected line 297
11. lemma OAI.CompleteCrouzeix.invertedExterior_frontier line 302
12. lemma OAI.CompleteCrouzeix.local_side_frontier line 324
13. lemma OAI.CompleteCrouzeix.invertedExterior_mem_closure_iff line 341
14. lemma OAI.CompleteCrouzeix.invertedExterior_frontier_iff line 365