OAI/Analysis/BiholderTransport/Coordinates/SplitLogInjective.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.prefix_log_fderiv_injective line 22
2. def OAI.WeakMTWTransport.coordinateEndpoint line 77
3. def OAI.WeakMTWTransport.coordinateEndpointVertical line 82
4. lemma OAI.WeakMTWTransport.coordinateEndpoint_contDiffAt line 86
5. lemma OAI.WeakMTWTransport.tangent_chart_fiber_inverse line 108
6. lemma OAI.WeakMTWTransport.coordinateEndpointVertical_apply line 123