OAI/Geometry/SmoothYau/Smoothness/FourLiftThreeSmul.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.metricPullbackInner line 15
2. lemma OAI.YauCounterexamples.metricPullbackInner_smooth line 20
3. def OAI.YauCounterexamples.fourProductInner line 54
4. lemma OAI.YauCounterexamples.fourProductInner_apply line 58
5. lemma OAI.YauCounterexamples.fourProductInner_pos line 65
6. lemma OAI.YauCounterexamples.fourProductInner_bounded line 76
7. lemma OAI.YauCounterexamples.fourProductInner_smooth line 95
8. def OAI.YauCounterexamples.fourProductMetric line 114