OAI/Geometry/SmoothYau/Smoothness/FlowInitialFderiv.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.YauCounterexamples.smooth_extension_near_compact line 28
2. theorem OAI.YauCounterexamples.smooth_local_flow_of_lipschitz line 84
3. lemma OAI.YauCounterexamples.flow_initial_fderiv line 150
4. lemma OAI.YauCounterexamples.flow_fderiv_time line 172
5. theorem OAI.YauCounterexamples.smooth_flowbox_of_lipschitz line 181
6. theorem OAI.YauCounterexamples.smooth_flowbox line 265
7. theorem OAI.YauCounterexamples.smooth_first_integral line 282