OAI/Analysis/BiholderTransport/LocalFlow/SmoothIntegralCurve.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.exists_smooth_local_manifold_flowline 79 - def
OAI.WeakMTWTransport.completeFlowline 127 - lemma
OAI.WeakMTWTransport.completeFlow_zeroline 130 - lemma
OAI.WeakMTWTransport.completeFlow_curveline 133 - lemma
OAI.WeakMTWTransport.completeFlow_addline 140 - lemma
OAI.WeakMTWTransport.completeFlow_eq_localline 150 - lemma
OAI.WeakMTWTransport.completeFlow_smooth_stepline 161 - lemma
OAI.WeakMTWTransport.contMDiff_completeFlow_time_sliceline 177 - lemma
OAI.WeakMTWTransport.contMDiff_completeFlowline 214