OAI/Geometry/SmoothYau/Limits/FrameDualNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.metricFrameSet line 47
2. lemma OAI.YauCounterexamples.metricFrameSet_fiber_nonempty line 50
3. lemma OAI.YauCounterexamples.metricFrameSet_isClosed line 56
4. lemma OAI.YauCounterexamples.metricFrameSet_bound line 71
5. theorem OAI.YauCounterexamples.metricFrameSet_isCompact line 85
6. lemma OAI.YauCounterexamples.metricFrameSet_injective line 94
7. lemma OAI.YauCounterexamples.metricFrameSet_equiv line 104
8. lemma OAI.YauCounterexamples.metricFrameSet_inverse_continuousOn line 112
9. lemma OAI.YauCounterexamples.metricFrameSet_inverse_bound line 120