OAI/Geometry/IsometricImmersion/Flows/FlowExistence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Flow.modelSquare line 14
2. theorem OAI.SmoothLocal.Flow.modelSquare_isCompact line 16
3. theorem OAI.SmoothLocal.Flow.coordinatePoint_mem_modelSquare line 18
4. def OAI.SmoothLocal.Flow.flowField line 24
5. theorem OAI.SmoothLocal.Flow.flowField_hasDerivAt_y line 28
6. theorem OAI.SmoothLocal.Flow.exists_flowField_lipschitz line 34
7. theorem OAI.SmoothLocal.Flow.exists_cap_picard line 55
8. theorem OAI.SmoothLocal.Flow.exists_cap_trajectory line 76