OAI/Geometry/SmoothYau/Smoothness/BundleMetricInner.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.bundleMetricInner line 16
2. lemma OAI.YauCounterexamples.bundleMetricInner_apply line 22
3. lemma OAI.YauCounterexamples.bundleMetricInner_smooth line 28
4. def OAI.YauCounterexamples.bundlePullbackMetric line 54
5. def OAI.YauCounterexamples.bundleExp line 72
6. lemma OAI.YauCounterexamples.bundleExp_coordinates line 76
7. lemma OAI.YauCounterexamples.bundleExp_smooth line 90
8. lemma OAI.YauCounterexamples.bundleExp_injective line 109
9. def OAI.YauCounterexamples.exponentialMetric line 115