OAI/Analysis/BiholderTransport/Geodesics/NormalEndpointLog.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.minimizingEndpointChartParameters line 41
2. lemma OAI.WeakMTWTransport.isCompact_minimizingRays_between line 51
3. lemma OAI.WeakMTWTransport.continuousOn_riemannianExp_chart line 59
4. lemma OAI.WeakMTWTransport.continuousOn_endpointChartParameters line 66
5. lemma OAI.WeakMTWTransport.isCompact_minimizingEndpointChartParameters line 90
6. lemma OAI.WeakMTWTransport.tangent_symmL_trivialization line 104
7. lemma OAI.WeakMTWTransport.trivialization_mem_minimizingEndpointChartParameters line 112