OAI/Geometry/SmoothYau/DifferentialEq/MfderivReModelTarget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.reModelChartedSpace line 15
2. lemma OAI.YauCounterexamples.reModel_isManifold line 21
3. lemma OAI.YauCounterexamples.contMDiff_reModel_source line 54
4. lemma OAI.YauCounterexamples.contMDiff_reModel_target line 73
5. lemma OAI.YauCounterexamples.mfderiv_reModel_source line 101
6. lemma OAI.YauCounterexamples.mfderiv_reModel_target line 142