OAI/Geometry/SmoothYau/Limits/LocalMetricInverse.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.YauCounterexamples.LocalMetricInverse line 15
2. theorem OAI.YauCounterexamples.nonempty_localMetricInverse line 37
3. def OAI.YauCounterexamples.metricInversePatch line 43
4. lemma OAI.YauCounterexamples.isOpen_metricInversePatch line 47
5. lemma OAI.YauCounterexamples.mem_metricInversePatch line 52
6. theorem OAI.YauCounterexamples.exists_compact_metric_patches line 57