OAI/Geometry/PolarProducts/SmoothFlow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothODE.curve_injective line 24
2. theorem OAI.SmoothODE.curve_of_const_along line 44
3. theorem OAI.SmoothODE.curve_spaceTime_outside line 57
4. theorem OAI.SmoothODE.curve_spaceTime_mapsTo line 72
5. theorem OAI.SmoothODE.step_preserves_tensor_on line 102
6. theorem OAI.SmoothODE.homeomorph_pow_preserves_tensor_on line 167
7. theorem OAI.SmoothODE.exists_spaceTime_transport line 193