OAI/Geometry/SmoothYau/Limits/ManifoldChartPush.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.manifoldChartPush line 23
2. lemma OAI.YauCounterexamples.manifoldChartPush_apply line 27
3. lemma OAI.YauCounterexamples.manifoldChartPush_support line 34
4. lemma OAI.YauCounterexamples.manifoldChartPush_tsupport line 45
5. lemma OAI.YauCounterexamples.manifoldChartPush_compact line 52
6. lemma OAI.YauCounterexamples.contMDiff_manifoldChartPush line 58